cadet
cadet copied to clipboard
A fast and certifying solver for quantified Boolean formulas.
When I run the command `./configure && make`, I get a long error message that ends with: ``` collect2: error: ld returned 1 exit status make: *** [Makefile:31: cadet] Error...
Hi, I am wondering if you have extended ID (your work "Incremental Determinization for Quantifier Elimination and Functional Synthesis" in CAV19) in the current version of cadet?
This fixes compilation issues: ``` gcc -O3 -DNDEBUG -std=c11 ./src/active_clause_iterator.o ./src/aiger.o ./src/aiger_utils.o ./src/bit_vector.o ./src/c2_casesplits_control.o ./src/c2_clause_minimization.o ./src/c2_rl.o ./src/c2_simplify.o ./src/c2_traces.o ./src/c2_validate.o ./src/cadet2.o ./src/casesplits.o ./src/cegar.o ./src/certify_SAT.o ./src/certify_UNSAT.o ./src/certify_validate.o ./src/conflict_analysis.o ./src/debug.o ./src/examples.o ./src/float_vector.o ./src/heap.o...