added option to pass candidate functions by kuldeepmeel · Pull Request #34 · meelgroup/arjun

kuldeepmeel · 2026-02-22T18:26:31Z

This option can allow us to take candidate functions as input. Will be helpful to debug repair.

Update checker Fixing warning Renaming I guess improved Cleanup UPdate More sane depends_on Smaller AIGs NO need No slow Adding BW and BVA-XOR option

Update Fix

Update checker Fixing warning Renaming I guess improved Cleanup UPdate More sane depends_on Smaller AIGs NO need No slow Adding BW and BVA-XOR option

…ined vars

kuldeepmeel · 2026-02-23T08:12:30Z

I have also added more commits that set all the unsat defined variables as equal for unate check and also fix a segfault. I can separate into different pull requests as well. Let me know.

src/unate_def.cpp

msoos · 2026-02-23T23:30:35Z

OK, let me push a version of this to the code that is I think (more?) correct :) But I see where this is going, and indeed it's a LOT faster. I'll tag these commits with your name so it's clear I didn't come up with the idea myself :)

msoos · 2026-02-23T23:33:15Z

Sorry, I am pushing only the parts related to unate_def speedup to the code :) I will review and merge the rest separately.

msoos · 2026-02-23T23:43:03Z

OK, so with the fixed values added as constants, we get 2=3x speedup, and by replacing the SAT solver with CaDiCaL we get another 4-5x speedup, so 30 seconds for doing unate_def on trivial_query42_1344n.qdimacs.cnf becomes 2.2 seconds. So the performance bottleneck is maybe mostly gone? Nice catch about setting the values as hard clauses.

msoos · 2026-02-23T23:51:13Z

The unate_def for sortnetsort9.AE.stepl.011.qdimacs.cnf was 416 seconds, now it's 17.88 seconds.

For sdlx-fixpoint-8.qdimacs.cnf it was 4.32s now it's 4.11s

So we are definitely much faseter, but the speedup is not distributed evenly. It's very nice, though, thanks for this observation. I think we can live with this speed for the moment, we don't need Oracle.

msoos · 2026-02-23T23:53:19Z

I'll rebase this on the newest changes (my updates to unate_def) and then review & merge. Thanks! This will have to wait for tomorrow.

msoos · 2026-02-24T00:06:22Z

For sortnetsort9.AE.stepl.012.qdimacs.cnf we went from 3000+ seconds to 38s. Actually, 38s is still a bit much, but it's a lot more reasonable. I'll think about how it could be made better. Also, the solution cache is useless.

kuldeepmeel · 2026-02-24T02:00:41Z

Sorry, I had pushed from my work machine but forgot to mention it here, not to consider this for the pull request.

msoos · 2026-02-24T23:23:50Z

OK, I have imported all unate changes, made it cleaner (sampl_set is not needed, input works fine) and merged aig-shared-ptr-better-fix into it, so we could cleanly merge this. But I find this diff very messy. Maybe you can have a go at cleaning it up. I'll try to merge this tomorrow after I do my own cleanup, although I probably will only be able to merge some of it. It does more than one thing I think.

If you want to work on it, you need to pull.

msoos

I added some comments. I now kinda understand where this is coming from. It's a good idea to have candicate AIGs passed. But the way it's doing it is very messy. I can try to clean this up tomorrow evening CET time, or if you wanna have a go at it, that's even better. But as-is it's messy, because it complicates a lot of logic. I'll have a hard time adding new ideas, as I'd be afraid it breaks this somehow. I'll see what I can do to make this easier on the eye/brain. I can understand it as-is, but I'm worried it'll be hard to deal with later.

msoos · 2026-02-24T23:33:05Z

src/arjun.h

+    bool get_preserve_existing_defs() const { return preserve_existing_defs; }

 private:
+    bool preserve_existing_defs = false;


This should be true by default. I don't see why it needs to be false by default?

msoos · 2026-02-24T23:34:54Z

src/main.cpp

    cnf.get_var_types(conf.verb | verbose_debug_enabled, "start do_synthesis");
-    if (do_synth_bve && !cnf.synth_done()) {
+    if (!candidate_defs_file.empty()) {
+        cnf.set_preserve_existing_defs(true);


This should be default. When this candidate_defs_file is set, only then do we need this set to false.

Also, can't we just skip defining them completely, and use the definitions from the file? Then we wouldn't need to overwrite. I'd prefer that actually :)

So the reason I defined these is because there can be two cases: we are trying to overwrite definitions because another pass discovered new definition: for example, backward definability can discover one definition and then when we are doing BVE, we may want to overwrite them or preserve the earlier definition. Perhaps more acute is the case when a variable is detected to be unate but we also want to eliminate it via BVE.

msoos · 2026-02-24T23:36:34Z

src/interpolant.cpp

+  auto flush_terms = [&]() {
+      if (!same_op_started) return;
+      aig = combine_balanced(std::move(same_op_terms), same_op_is_and);
+      same_op_terms.clear();
+      same_op_started = false;
+  };


I believe this balanced thing is part of another PR, #35. Let's fix that up, and remove this from here, so we can work on these independently. I wanna push these all in, but I'd prefer to have them reviewed/fixed independently

msoos · 2026-02-24T23:40:45Z

src/manthan.cpp

 }

-void Manthan::fill_var_to_formula_with(set<uint32_t>& vars) {
+void Manthan::fill_var_to_formula_with_backward(const bool include_to_define) {


I think the case where we have include_to_define = true should be a separate function. It now does two very different things, and I'm a bit worried it'll be hard to understand. Code duplication is OK in this case, I think .The way it is now it's quite hard to tell what's going on.

msoos · 2026-02-25T19:52:20Z

The import_candidate_functions is buggy I think? The std::map<uint32_t, uint32_t> orig_to_current_new; almost surely should be var->Lit not var->var. This whole thing has zero tests and cannot be fuzzed. I'm sorry, I can't, there is no way we can check what this is doing, relying on this would be like relying on Manthanv2 to inform us about what to do. Just pure YOLO. I'll think about how this could be done. But as-is, it's a giant hack.

I will remove the possibility of doing a mapping in map_aigs_to_orig, and find a way to do it without that mapping. It's very dangerous, as you just have found out. It's a complicated piece of code. That var->var mapping I think is wrong.

msoos · 2026-02-25T19:53:25Z

Well, I didn't mean to close it to be honest, no idea how that happened. I see that we need to be able to do what this PR is doing. I just find this to be way too hacky. I'll think about it

msoos · 2026-02-25T20:27:35Z

OK, I am reopening and trying to find a way to do this right. We must be able to fuzz this.

added option to pass candidate functions

6f2d663

kuldeepmeel marked this pull request as draft February 22, 2026 18:43

msoos and others added 15 commits February 22, 2026 15:33

Adding an assert

547c4a4

Cleanup

3f180b4

Initial BVA

b2fa586

Update checker Fixing warning Renaming I guess improved Cleanup UPdate More sane depends_on Smaller AIGs NO need No slow Adding BW and BVA-XOR option

Silent var update

3405c7d

Update fuzzer to match new options

2779b72

Fixing bug about bw equal forcing

e5de3db

Let's set to 4, seems best

c5d9955

Update strategy matrix

189e4de

Update Fix

More fuzz

80a9fd4

edits

21976ff

Initial BVA

aa83290

Update checker Fixing warning Renaming I guess improved Cleanup UPdate More sane depends_on Smaller AIGs NO need No slow Adding BW and BVA-XOR option

Going back to old strategy numbering

5a6b7af

Fix strategy label after cherry-pick conflict resolution

812ac5e

Merge branch 'aig-shared-ptr-better-fix' into input_guesses

55941de

fixed numbering due to merge

5156579

kuldeepmeel marked this pull request as ready for review February 22, 2026 22:54

kuldeepmeel added 3 commits February 22, 2026 19:31

Use classified input set in unate synthesis

31dd021

balanced AIG construction to avoid segfault due to deep recursion

a616cfb

rerun backward synthesis after unate_def with dependency-aware predef…

860aefc

…ined vars

moving from assumptions to clauses

6c38c9c

msoos reviewed Feb 23, 2026

View reviewed changes

src/unate_def.cpp Show resolved Hide resolved

edits

091121c

kuldeepmeel force-pushed the input_guesses branch from 091121c to 860aefc Compare February 24, 2026 02:41

msoos added 3 commits February 24, 2026 23:48

Merge branch 'input_guesses' into tmp

ad8f088

Cleanup unate_def

53602a1

Merge branch 'aig-shared-ptr-better-fix' into input_guesses-fixes

b4279c8

msoos requested changes Feb 24, 2026

View reviewed changes

msoos closed this Feb 25, 2026

Merge

b8daad2

msoos reopened this Feb 25, 2026

msoos added 4 commits February 25, 2026 21:29

Taking out the part that is balancing AIGs

d858259

Fixing mapping

68ca086

Update

76af7e0

Merge branch 'aig-shared-ptr-better-fix' into input_guesses

0c1d685

Conversation

kuldeepmeel commented Feb 22, 2026

Uh oh!

kuldeepmeel commented Feb 23, 2026

Uh oh!

Uh oh!

msoos commented Feb 23, 2026

Uh oh!

msoos commented Feb 23, 2026

Uh oh!

msoos commented Feb 23, 2026

Uh oh!

msoos commented Feb 23, 2026

Uh oh!

msoos commented Feb 23, 2026

Uh oh!

msoos commented Feb 24, 2026

Uh oh!

kuldeepmeel commented Feb 24, 2026

Uh oh!

msoos commented Feb 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

msoos left a comment

Choose a reason for hiding this comment

Uh oh!

msoos Feb 24, 2026

Choose a reason for hiding this comment

Uh oh!

msoos Feb 24, 2026

Choose a reason for hiding this comment

Uh oh!

kuldeepmeel Feb 26, 2026

Choose a reason for hiding this comment

Uh oh!

msoos Feb 24, 2026

Choose a reason for hiding this comment

Uh oh!

msoos Feb 24, 2026

Choose a reason for hiding this comment

Uh oh!

msoos commented Feb 25, 2026

Uh oh!

msoos commented Feb 25, 2026

Uh oh!

msoos commented Feb 25, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

msoos commented Feb 24, 2026 •

edited

Loading