Merge branch 'feat/simple_projection'

cadet.xcodeproj/project.pbxproj

@@ -8,7 +8,6 @@
 
 /* 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 */; };
@@ -159,7 +158,6 @@
 		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>"; };
@@ -314,7 +312,6 @@
 				28DA30F31DFFDD2600EABCA6 /* skolem_dependencies.h */,
 				28DA30F21DFFDD2600EABCA6 /* skolem_dependencies.c */,
 				28FEE64A1EDA304000A9D8CA /* skolem_conflict_analysis.c */,
-				28715A1220B3E5780047F481 /* skolem_encodings.c */,
 			);
 			name = skolem;
 			sourceTree = "<group>";
@@ -532,7 +529,6 @@
 				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 */,

scripts/run.py

@@ -80,10 +80,10 @@ def get_paths_from_categories(categories, directory):
             omitted_files = 0
             detected_files = 0
             for filename in filenames:
-                if filename.endswith('qdimacs.gz') or \
-                   filename.endswith('aag') or \
-                   filename.endswith('aig') or \
-                   filename.endswith('qdimacs'):
+                if filename.endswith('.qdimacs.gz') or \
+                   filename.endswith('.aag') or \
+                   filename.endswith('.aig') or \
+                   filename.endswith('.qdimacs'):
 
                     paths[os.path.join(dirpath,filename)] = (os.path.join(dirpath,filename), 30)
                     detected_files += 1
@@ -326,12 +326,16 @@ def run_jobs(jobs, timeout, threads=1, manage_certificate=False):
         try:
             job_name, job, expected, result = result_queue.get(block=True)
             results[job_name] = result
+            seconds = None
+            memory = None
+            return_value = None
 
-            seconds = result['seconds']
-            memory = result['memory']
-            return_value = result['return_value']
+            if result is not None:
+                seconds = result['seconds']
+                memory = result['memory']
+                return_value = result['return_value']
 
-            if seconds is None:
+            if result is not None and seconds is None:
                 log_progress(yellow('TIMEOUT: '))
                 TIMEOUTS += 1
             elif return_value == 30:

scripts/tester.py

@@ -577,7 +577,7 @@ def get_benchmark_result(testcase, time_output):
                    '--rl --rl_mock --sat_by_qbf --debugging --minimize --rl_vsids_rewards',
                    '--rl --rl_mock --sat_by_qbf --random_decisions --rl_vsids_rewards',
                    '--rl --rl_mock --sat_by_qbf --random_decisions --rl_advanced_rewards --rl_vsids_rewards --rl_slim_state',
-                   '--debugging --cegar_soft_conflict_limit -l 10 --sat_by_qbf --random_decisions --fresh_seed'
+                   '--debugging -l 10 --sat_by_qbf --random_decisions --fresh_seed'
                    ]
 
     if ARGS.config:

src/cadet2.c

@@ -542,15 +542,11 @@ void c2_run(C2* c2, unsigned remaining_conflicts) {
                 return;
             } else { // take a decision
                 assert(!skolem_is_conflicted(c2->skolem));
-
                 if (c2->restarts >= c2->magic.num_restarts_before_Jeroslow_Wang && !c2->options->reinforcement_learning) {
-
                     float pos_JW_weight = c2_Jeroslow_Wang_log_weight(&decision_var->pos_occs);
                     float neg_JW_weight = c2_Jeroslow_Wang_log_weight(&decision_var->neg_occs);
-
                     phase = pos_JW_weight > neg_JW_weight ? 1 : -1;
                 }
-
                 c2_scale_activity(c2, decision_var->var_id, c2->magic.decision_var_activity_modifier);
 
                 // Pushing before the actual decision is important to keep things
@@ -716,6 +712,36 @@ cadet_res c2_sat(C2* c2) {
     abortif(int_vector_count(c2->skolem->universals_assumptions) != 0, "There are universal assumptions before solving started.");
     assert(c2->options->functional_synthesis || int_vector_count(c2->qcnf->universal_clauses) == 0); // they must have been detected through c2_new_clause
 
+    if (c2->options->functional_synthesis) {
+        int_vector* tmp_vars = int_vector_init();
+        for (unsigned i = 0; i < var_vector_count(c2->qcnf->vars); i++) {
+            int_vector_add(tmp_vars, 0);
+        }
+        for (unsigned i = 0; i < vector_count(c2->qcnf->all_clauses); i++) {
+            Clause* c = vector_get(c2->qcnf->all_clauses, i);
+            V3("Satsolver clause:");
+            for (unsigned j = 0; j < c->size; j++) {
+                Lit l = c->occs[j];
+                unsigned var_id = lit_to_var(l);
+                if (qcnf_is_universal(c2->qcnf, var_id)) {
+                    int satlit = skolem_get_satsolver_lit(c2->skolem, l);
+                    satsolver_add(c2->skolem->skolem, satlit);
+                    V3("%d(u%d)\n", satlit, l);
+                } else {
+                    if (! int_vector_get(tmp_vars, var_id)) {
+                        int_vector_set(tmp_vars, var_id, satsolver_inc_max_var(c2->skolem->skolem));
+                    }
+                    int sign = l>0 ? 1 : -1;
+                    int satlit = int_vector_get(tmp_vars, var_id);
+                    satsolver_add(c2->skolem->skolem, sign * satlit);
+                    V3("%d(e%d)\n", sign * satlit, l);
+                }
+            }
+            satsolver_clause_finished(c2->skolem->skolem);
+        }
+        int_vector_free(tmp_vars);
+    }
+
     V1("Initial propagation\n");
     c2_propagate(c2);
     if (c2_is_in_conflcit(c2)) {
@@ -762,11 +788,6 @@ cadet_res c2_sat(C2* c2) {
             c2_restart_heuristics(c2);
             if (c2->options->minimize_learnt_clauses) {c2_simplify(c2);}
         }
-
-        if (c2->options->cegar_soft_conflict_limit && c2->statistics.conflicts > 1000 && ! c2->options->cegar) {
-            LOG_WARNING("Switching cegar on after >1000 conflicts to save time during generation of problems for RL. Remove for normal operation.\n");
-            c2->options->cegar = true;
-        }
     }
 return_result:
     assert(true);
@@ -812,7 +833,7 @@ cadet_res c2_solve_qdimacs(const char* file_name, Options* options) {
     }
     C2* c2 = c2_from_file(file, options);
     close_possibly_zipped_file(file_name, file);
-
+    
     V1("Maximal variable index: %u\n", var_vector_count(c2->qcnf->vars));
     V1("Number of clauses: %u\n", vector_count(c2->qcnf->all_clauses));
     V1("Number of scopes: %u\n", vector_count(c2->qcnf->scopes));

src/certify_SAT.c

@@ -228,7 +228,8 @@ unsigned cert_encode_conflicts(Skolem* skolem, aiger* a, unsigned *max_sym, int_
 }
 
 // Certify all vars with dlvl>0 by writing out the unique consequences in the correct order
-void cert_encode_function_for_case(Skolem* skolem, aiger* a, unsigned *max_sym, int_vector* aigerlits,
+void cert_encode_function_for_case(Skolem* skolem, aiger* a, unsigned *max_sym,
+                                   int_vector* aigerlits,
                                    int_vector* decisions,
                                    int_vector* unique_consequences) {
     if (debug_verbosity >= VERBOSITY_MEDIUM) {V2("Decision order: "); int_vector_print(decisions); V2("\n");}
@@ -249,11 +250,13 @@ void cert_encode_function_for_case(Skolem* skolem, aiger* a, unsigned *max_sym,
 
 unsigned cert_dlvl0_definitions(aiger* a, int_vector* aigerlits, Skolem* skolem, unsigned* max_sym) {
     int_vector* decision_sequence = case_splits_determinization_order_with_polarities(skolem);
-    cert_encode_function_for_case(skolem, a, max_sym, aigerlits, decision_sequence, skolem->unique_consequence);
+    cert_encode_function_for_case(skolem, a, max_sym, aigerlits, decision_sequence,
+                                  skolem->unique_consequence);
 
     if (skolem->options->quantifier_elimination) {
         unsigned res = cert_encode_conflicts(skolem, a, max_sym, aigerlits, decision_sequence,
-                                             skolem->potentially_conflicted_variables, skolem->unique_consequence);
+                                             skolem->potentially_conflicted_variables,
+                                             skolem->unique_consequence);
         int_vector_free(decision_sequence);
         return res;
     } else {
@@ -433,6 +436,7 @@ void c2_write_AIG_certificate(C2* c2) {
         }
     }
 
+    bool valid = false;
     if (c2->options->quantifier_elimination) {
         // This is the quantifier elimination certificate.
         // There are three ways the resulting formula can evaluate to false:
@@ -467,9 +471,11 @@ void c2_write_AIG_certificate(C2* c2) {
         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);
-        abortif(!valid, "Quantifier elimination failed!");
-
+        if (c2->options->verify) {
+            valid = cert_validate_quantifier_elimination(a, c2->qcnf, aigerlits, projection);
+        } else {
+            valid = true;
+        }
     } else { // Create function
         int_vector* out_aigerlits = int_vector_copy(aigerlits);
         for (unsigned var_id = 0; var_id < vector_count(case_aigerlits); var_id++) {
@@ -492,19 +498,20 @@ void c2_write_AIG_certificate(C2* c2) {
 
         cert_define_aiger_outputs(skolem_dlvl0, a, out_aigerlits);
 
-        if (!c2->options->functional_synthesis) {
-            bool valid = cert_validate_skolem_function(a, c2->qcnf, out_aigerlits, case_selectors);
-            abortif(!valid, "Skolem function invalid!");
+        if (!c2->options->verify) {
+            valid = true;
+        } else if (!c2->options->functional_synthesis) {
+            valid = cert_validate_skolem_function(a, c2->qcnf, out_aigerlits, case_selectors);
         } else {
-            bool valid = cert_validate_functional_synthesis(a, c2->qcnf, out_aigerlits, case_selectors);
-            abortif(!valid, "Functional synthesis failed!");
+            valid = cert_validate_functional_synthesis(a, c2->qcnf, out_aigerlits, case_selectors);
         }
 
         int_vector_free(out_aigerlits);
     }
-
     cert_write_aiger(a, c2->options);
 
+    abortif(!valid, "Validation of certificate invalid!");
+
     int_vector_free(aigerlits);
     vector_free(case_aigerlits);
     int_vector_free(case_selectors);

src/main.c

@@ -169,8 +169,6 @@ int main(int argc, const char* argv[]) {
                         options->reinforcement_learning = true;
                         log_colors = false;
                         options->reinforcement_learning_mock = true;
-                    } else if (strcmp(argv[i], "--cegar_soft_conflict_limit") == 0) {
-                        options->cegar_soft_conflict_limit = true;
                     } else if (strcmp(argv[i], "--trace_for_profiling") == 0) {
                         options->trace_for_profiling = true;
                     } else if (strcmp(argv[i], "--print_variable_names") == 0) {
@@ -194,6 +192,8 @@ int main(int argc, const char* argv[]) {
                         options->enhanced_pure_literals = ! options->enhanced_pure_literals;
                     } else if (strcmp(argv[i], "--qbce") == 0) {
                         options->qbce = ! options->qbce;
+                    } else if (strcmp(argv[i], "--dontverify") == 0) {
+                        options->verify = 0;
                     } else {
                         LOG_ERROR("Unknown long argument '%s'", argv[i]);
                         print_usage(argv[0]);

src/options.c

@@ -66,9 +66,8 @@ Options* default_options() {
     o->rl_vsids_rewards = false;
     o->rl_slim_state = false;
     o->reinforcement_learning_mock = false;
-    o->cegar_soft_conflict_limit = false;
     o->hard_decision_limit = 0;  // 0 means no limit
-
+    o->verify = 1;
     return o;
 }
 
@@ -113,8 +112,9 @@ char* options_get_help() {
     "\t--trace_for_vis\t\tPrint trace of solver states at every conflict point.\n"
     "\t--trace_for_profiling\tPrint trace of learnt clauses with timestamps\n\t\t\t\tand SAT solver time consumption.\n"
     "\t--print_variable_names\tReplace variable numbers by names where available\n\t\t\t\t(default %d)\n"
+    "\t--dontverify\t\tDo not verify results.\n"
     "\n  Aiger options\n"
-    "\t----aiger_controllable_inputs [string]\tSet prefix of controllable inputs in QAIGER\n\t\t\t\t(default '%s')\n"
+    "\t--aiger_controllable_inputs [string]\tSet prefix of controllable inputs in QAIGER\n\t\t\t\t(default '%s')\n"
     "\n",
     debug_verbosity,
     o->reinforcement_learning,

src/options.h

@@ -28,8 +28,8 @@ typedef struct {
     bool rl_vsids_rewards;
     bool rl_slim_state;
     bool reinforcement_learning_mock; // for testing reinforcement learning code
-    bool cegar_soft_conflict_limit; // switches cegar on after 1000 conflicts to also solve hard problems.
     unsigned hard_decision_limit;
+    bool verify;
 
     // Use a configuration of CADET 2 that is easier to debug than the
     // performance-oriented configuration

src/satsolver_picosat_assumptions.c

@@ -171,7 +171,7 @@ void satsolver_add(SATSolver* solver, int lit) {
 
 #ifdef SATSOLVER_TRACE
     if (solver->trace_solver_commands) {
-        LOG_PRINTF("picosat_add(s,%d);\n",pico_lit);
+        LOG_PRINTF("picosat_add(s,%d); // was lit %d \n", pico_lit, lit);
     }
 #endif
 }
@@ -487,7 +487,7 @@ void satsolver_print_statistics(SATSolver* solver) {
     V0("  PicoSAT maxvar: %u\n", picosat_inc_max_var(solver->ps));
 #ifdef SATSOLVER_TRACE
     if (solver->trace_solver_commands) {
-        abortif(true,"Not logging satsolver_print_statistics, implement me.");
+        LOG_PRINTF("//call to picosat_inc_vax_var for printing statistics.\n");
     }
 #endif
 }