debugged the new projection functionality

cadet.xcodeproj/project.pbxproj

@@ -8,6 +8,7 @@
 
 /* Begin PBXBuildFile section */
 		28675A4F1DDAA9D000951212 /* main.c in Sources */ = {isa = PBXBuildFile; fileRef = 28675A1C1DDAA9D000951212 /* main.c */; };
+		28715A1320B3E5780047F481 /* skolem_encodings.c in Sources */ = {isa = PBXBuildFile; fileRef = 28715A1220B3E5780047F481 /* skolem_encodings.c */; };
 		289A56E0207EF58100BEAC53 /* qcnf_variable_names.c in Sources */ = {isa = PBXBuildFile; fileRef = 289A56DF207EF58100BEAC53 /* qcnf_variable_names.c */; };
 		28DC3AD72079960E00266A75 /* certify_validate.c in Sources */ = {isa = PBXBuildFile; fileRef = 28DC3AD62079960E00266A75 /* certify_validate.c */; };
 		28FF2E86206C285100AEFB7F /* log.c in Sources */ = {isa = PBXBuildFile; fileRef = 28675A6B1DDAAB2600951212 /* log.c */; };
@@ -158,6 +159,7 @@
 		28675A431DDAA9D000951212 /* vector.c */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.c.c; name = vector.c; path = src/vector.c; sourceTree = "<group>"; };
 		28675A441DDAA9D000951212 /* vector.h */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.c.h; name = vector.h; path = src/vector.h; sourceTree = "<group>"; };
 		28675A6B1DDAAB2600951212 /* log.c */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.c.c; name = log.c; path = src/log.c; sourceTree = "<group>"; };
+		28715A1220B3E5780047F481 /* skolem_encodings.c */ = {isa = PBXFileReference; lastKnownFileType = sourcecode.c.c; name = skolem_encodings.c; path = src/skolem_encodings.c; sourceTree = "<group>"; };
 		287BB7C11E0609B000AAE180 /* partitions.c */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.c.c; name = partitions.c; path = src/partitions.c; sourceTree = "<group>"; };
 		287C3B0B1E37EF7B00F7096A /* examples.c */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.c.c; name = examples.c; path = src/examples.c; sourceTree = "<group>"; };
 		287C3B0C1E37EF7B00F7096A /* examples.h */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.c.h; name = examples.h; path = src/examples.h; sourceTree = "<group>"; };
@@ -312,6 +314,7 @@
 				28DA30F31DFFDD2600EABCA6 /* skolem_dependencies.h */,
 				28DA30F21DFFDD2600EABCA6 /* skolem_dependencies.c */,
 				28FEE64A1EDA304000A9D8CA /* skolem_conflict_analysis.c */,
+				28715A1220B3E5780047F481 /* skolem_encodings.c */,
 			);
 			name = skolem;
 			sourceTree = "<group>";
@@ -529,6 +532,7 @@
 				28FF2EAB206C285100AEFB7F /* satsolver_picosat_assumptions.c in Sources */,
 				28FF2EA5206C285100AEFB7F /* lglib.c in Sources */,
 				28FF2E91206C285100AEFB7F /* c2_clause_minimization.c in Sources */,
+				28715A1320B3E5780047F481 /* skolem_encodings.c in Sources */,
 				28FF2EB9206C285100AEFB7F /* val_vector.c in Sources */,
 				28FF2EB1206C285100AEFB7F /* heap.c in Sources */,
 				28FF2E9F206C285100AEFB7F /* examples.c in Sources */,

integration-tests/constants_and_elimination.qdimacs

@@ -0,0 +1,6 @@
+p cnf 3 3
+a 3 0
+e 1 2 0
+-2 -1 0
+2 3 0
+2 1 0

src/aiger_utils.c

@@ -36,6 +36,7 @@ bool is_negated(unsigned signal) {
     return signal % 2; // negation is encoded in the last bit
 }
 
+// Negates aiger signals
 unsigned negate(unsigned signal) {
     return signal ^ 1; // flipping the last bit with xor
 }

src/cadet2.c

@@ -1,3 +1,4 @@
+
 //
 //  cadet2.c
 //  cadet
@@ -709,7 +710,14 @@ cadet_res c2_sat(C2* c2) {
     V1("Initial propagation\n");
     c2_propagate(c2);
     if (c2_is_in_conflcit(c2)) {
-        abortif(c2->options->functional_synthesis, "In conflict mode before taking any decisions");
+
+        if (c2->options->functional_synthesis) {
+            V1("In conflict before any decision was taken. This formula is equivalent to false.")
+            assert(c2->skolem->state == SKOLEM_STATE_CONSTANTS_CONLICT);
+            c2_add_lit(c2, 0);  // make formula false
+            c2->state = C2_SAT;
+            goto return_result;
+        }
 
         c2->state = C2_UNSAT;
         goto return_result;

src/certify_SAT.c

@@ -374,7 +374,7 @@ void c2_write_AIG_certificate(C2* c2) {
     assert(c2->options->certificate_type != QBFCERT || max_sym == var2aigerlit(a->maxvar + 1));
 
     // Certificate for the dlvl0 variables
-    unsigned dlvl0_conflict = cert_dlvl0_definitions(a, aigerlits, skolem_dlvl0, &max_sym);
+    unsigned dlvl0_conflict_aigerlit = cert_dlvl0_definitions(a, aigerlits, skolem_dlvl0, &max_sym);
 
     // The following data structures remember all the aigerlits for all cases; dlvl0 vars are only remembered once
     vector* case_aigerlits = vector_init(); // stores for every variable an int_vector of aigerlits for the different cases
@@ -404,7 +404,7 @@ void c2_write_AIG_certificate(C2* c2) {
                                                         c->potentially_conflicted_variables,
                                                         c->unique_consequences));
         }
-        abortif(! c2->options->cegar && case_applies == aiger_false, "This case does not contribute.");
+        abortif(!c2->options->functional_synthesis && ! c2->options->cegar && case_applies == aiger_false, "This case does not contribute.");
 
 //        // Adding auxiliary outputs to the circuit to simplify debugging.
 //        // These outputs violate output standards, so do not use otherwise.
@@ -464,7 +464,7 @@ void c2_write_AIG_certificate(C2* c2) {
         }
 
         unsigned projection = aigeru_AND(a, &max_sym, some_case_applies, negate(some_universal_violated));
-        projection = aigeru_AND(a, &max_sym, projection, negate(dlvl0_conflict));
+        projection = aigeru_AND(a, &max_sym, projection, negate(dlvl0_conflict_aigerlit));
         aiger_add_output(a, projection, QUANTIFIER_ELIMINATION_OUTPUT_STRING);
 
         bool valid = cert_validate_quantifier_elimination(a, c2->qcnf, aigerlits, projection);

src/satsolver.h

@@ -48,6 +48,7 @@ int  satsolver_inc_max_var(SATSolver*);
 void satsolver_set_max_var(SATSolver*, int new_max);
 int satsolver_get_max_var(SATSolver*);
 void satsolver_add(SATSolver*, int lit);
+void satsolver_add_all(SATSolver* solver, int_vector* lits);
 void satsolver_assume(SATSolver*, int lit);
 void satsolver_clear_assumptions(SATSolver*);
 bool satsolver_inconsistent(SATSolver*);

src/satsolver_picosat_assumptions.c

@@ -176,6 +176,15 @@ void satsolver_add(SATSolver* solver, int lit) {
 #endif
 }
 
+void satsolver_add_all(SATSolver* solver, int_vector* lits) {
+    assert(lits);
+    for (unsigned i = 0; i < int_vector_count(lits); i++) {
+        int lit = int_vector_get(lits, i);
+        assert(lit != 0);
+        satsolver_add(solver, lit);
+    }
+}
+
 void satsolver_clause_finished(SATSolver* solver) {
     satsolver_clause_finished_for_context(solver, int_vector_count(solver->context_literals)); // used as proxy for push_count
 }

src/skolem.c

@@ -336,6 +336,7 @@ int skolem_get_satsolver_lit(Skolem* s, Lit lit) {
 int skolem_get_depends_on_decision_satlit(Skolem* s, unsigned var_id) {
     assert(var_id != 0);
     skolem_var si = skolem_get_info(s, var_id);
+    assert(si.depends_on_decision_satlit != 0);
     return si.depends_on_decision_satlit;
 }
 
@@ -752,6 +753,7 @@ void skolem_propagate_pure_variable(Skolem* s, unsigned var_id) {
             }
             skolem_update_deterministic(s, var_id);
             skolem_update_dependencies(s, var_id, skolem_compute_dependencies(s,var_id));
+
         } else {
             // pure and locally conflicted
             skolem_fix_lit_for_unique_antecedents(s,   pure_polarity * (Lit) var_id, true);
@@ -1158,7 +1160,7 @@ void skolem_undo(void* parent, char type, void* obj) {
         case SKOLEM_OP_UPDATE_INFO_DEPENDS_ON_DECISION_SATLIT:
             si = skolem_var_vector_get(s->infos, suu.sus.var_id);
             si->depends_on_decision_satlit = suu.sus.val;
-            assert(si->depends_on_decision_satlit == 0);
+//            assert(si->depends_on_decision_satlit == 0);
             break;
 
         default:
@@ -1282,12 +1284,12 @@ void skolem_assign_constant_value(Skolem* s, Lit lit, union Dependencies propaga
     // Propagation of constant may be in conflict with existing definitions
     //        assert(!skolem_is_deterministic(s, lit_to_var(lit)));
     assert(lit != 0);
-    unsigned var_id = lit_to_var(lit);
     assert(!skolem_is_conflicted(s));
 //    assert(skolem_get_satsolver_lit(s, lit) != s->satlit_true); // not constant already, not a big problem, but why should this happen?
     abortif(skolem_get_satsolver_lit(s, -lit) == s->satlit_true, "Propagation ended in inconsistent state.\n");
 
     V3("Skolem: Assign value %d.\n", lit);
+    unsigned var_id = lit_to_var(lit);
     skolem_update_reason_for_constant(s, var_id, reason ? reason->clause_idx : INT_MAX, s->decision_lvl);
 
     if (propagation_deps.dependence_lvl == 1) {
@@ -1431,7 +1433,9 @@ void skolem_propagate_constants_over_clause(Skolem* s, Clause* c) {
         skolem_update_state(s, SKOLEM_STATE_CONSTANTS_CONLICT);
         stack_push_op(s->stack, SKOLEM_OP_PROPAGATION_CONFLICT, NULL);
 
-        V3("Conflict in explicit propagation in skolem domain for clause %u and var %u\n", s->conflicted_clause->clause_idx, s->conflict_var_id);
+        V3("Conflict in explicit propagation in skolem domain for clause %u and var %u\n",
+           s->conflicted_clause->clause_idx,
+           s->conflict_var_id);
 
     } else { // assign value
 //        if (qcnf_is_universal(s->qcnf, lit_to_var(unassigned_lit)) &&
@@ -1532,11 +1536,12 @@ void skolem_decision(Skolem* s, Lit decision_lit) {
 
         // encode depends_on_decision_satlit
         // actual := old || (-val && -opposite)
-        // onesided only: (val && -old) || (opposite && -old) => - actual
+        // onesided only: actual => (old || (-val && -opposite))
+        // simplify: -actual || old || (-val && -opposite)
+        // in CNF:
         skolem_encode_depends_on_decision(s, decision_var_id);
-        int actual_depends_on_decision_satlit = satsolver_inc_max_var(s->skolem);
         int old_depends_on_decision_satlit = skolem_get_depends_on_decision_satlit(s, decision_var_id);
-        skolem_update_depends_on_decision_satlit(s, decision_var_id, actual_depends_on_decision_satlit);
+        int actual_depends_on_decision_satlit = satsolver_inc_max_var(s->skolem);
 
         satsolver_add(s->skolem, - val_satlit);
         satsolver_add(s->skolem, old_depends_on_decision_satlit);
@@ -1547,6 +1552,8 @@ void skolem_decision(Skolem* s, Lit decision_lit) {
         satsolver_add(s->skolem, old_depends_on_decision_satlit);
         satsolver_add(s->skolem, - actual_depends_on_decision_satlit);
         satsolver_clause_finished(s->skolem);
+
+        skolem_update_depends_on_decision_satlit(s, decision_var_id, actual_depends_on_decision_satlit);
     }
 
     // Decision variable needs to be deterministic before we can do conflict checks. Also this is why we have to check exactly here.

src/skolem_encodings.c

@@ -7,6 +7,7 @@
 //
 
 #include "skolem.h"
+#include "log.h"
 
 // Returns a satlit that can only be true if the uc is fired and depends on a decision
 int skolem_encode_uc_depends_on_decision(Skolem* s, Clause* c) {
@@ -42,27 +43,41 @@ int skolem_encode_uc_depends_on_decision(Skolem* s, Clause* c) {
 }
 
 
-static void skolem_encode_depends_helper(Skolem *s, Lit lit) {
+static int_vector* skolem_encode_depends_helper(Skolem *s, Lit lit) {
     vector* occs = qcnf_get_occs_of_lit(s->qcnf, lit);
+    int_vector* clause_depends_literals = int_vector_init();
     for (unsigned i = 0; i < vector_count(occs); i++) {
         Clause* c = vector_get(occs, i);
         if (skolem_get_unique_consequence(s, c) == lit) {
             int uc_depends = skolem_encode_uc_depends_on_decision(s, c);
-            satsolver_add(s->skolem, - uc_depends);
+            int_vector_add(clause_depends_literals, uc_depends);
+            V4("Clause %u gets depends lit %d\n", c->clause_idx, uc_depends);
         }
     }
+    return clause_depends_literals;
 }
 
 
 void skolem_encode_depends_on_decision(Skolem* s, unsigned var_id) {
     if (!s->options->functional_synthesis) {
         return;
     }
-    int satlit = satsolver_inc_max_var(s->skolem);
-    skolem_encode_depends_helper(s,   (Lit) var_id);
-    skolem_encode_depends_helper(s, - (Lit) var_id);
-    satsolver_add(s->skolem, - satlit);
+
+    int_vector* cd_lits1 = skolem_encode_depends_helper(s,   (Lit) var_id);
+    int_vector* cd_lits2 = skolem_encode_depends_helper(s, - (Lit) var_id);
+    satsolver_add_all(s->skolem, cd_lits1); // adding them now since previous call contains satsolver clauses.
+    satsolver_add_all(s->skolem, cd_lits2);
+    int_vector_free(cd_lits1);
+    int_vector_free(cd_lits2);
+
+    int old_depends_on_decision_satlit = skolem_get_depends_on_decision_satlit(s, var_id);
+    if (old_depends_on_decision_satlit != - s->satlit_true) {
+        satsolver_add(s->skolem, old_depends_on_decision_satlit);
+    }
+
+    int new_depends_on_decision_satlit = satsolver_inc_max_var(s->skolem);
+    satsolver_add(s->skolem, - new_depends_on_decision_satlit);
     satsolver_clause_finished(s->skolem);
 
-    skolem_update_depends_on_decision_satlit(s, var_id, satlit);
+    skolem_update_depends_on_decision_satlit(s, var_id, new_depends_on_decision_satlit);
 }

src/skolem_var.c

@@ -116,7 +116,7 @@ void skolem_enlarge_skolem_var_vector(Skolem* s, unsigned var_id) {
     sv.decision_pos = 0;
     sv.decision_neg = 0;
 
-    sv.depends_on_decision_satlit = 0;
+    sv.depends_on_decision_satlit = - s->satlit_true;
 
     sv.dep = s->empty_dependencies;
 
@@ -277,7 +277,7 @@ void skolem_update_decision(Skolem* s, Lit lit) {
 void skolem_update_depends_on_decision_satlit(Skolem* s, unsigned var_id, int satlit) {
     skolem_enlarge_skolem_var_vector(s, var_id);
     skolem_var* sv = skolem_var_vector_get(s->infos, var_id);
-    assert(sv->depends_on_decision_satlit == 0);
+    assert(satlit != 0);
 
     V4("Setting depends_on_decision_satlit %d for var %u\n", satlit, var_id);
     union skolem_undo_union suu;