From 419b07b4ae0c885ec2817112c72ce3d169504cff Mon Sep 17 00:00:00 2001 From: Markus N Rabe Date: Sun, 23 Dec 2018 16:42:01 +0100 Subject: [PATCH 1/7] implemented new functional synthesis mode; removed cegar soft decision limit --- cadet.xcodeproj/project.pbxproj | 4 - src/cadet2.c | 39 ++++-- src/certify_SAT.c | 22 ++-- src/main.c | 2 - src/options.c | 1 - src/options.h | 1 - src/satsolver_picosat_assumptions.c | 4 +- src/skolem.c | 26 +--- src/skolem.h | 5 +- src/skolem_encodings.c | 196 ---------------------------- src/skolem_var.c | 13 -- src/skolem_var.h | 1 - 12 files changed, 47 insertions(+), 267 deletions(-) delete mode 100644 src/skolem_encodings.c diff --git a/cadet.xcodeproj/project.pbxproj b/cadet.xcodeproj/project.pbxproj index 400c52b..c804d83 100644 --- a/cadet.xcodeproj/project.pbxproj +++ b/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 = ""; }; 28675A441DDAA9D000951212 /* vector.h */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.c.h; name = vector.h; path = src/vector.h; sourceTree = ""; }; 28675A6B1DDAAB2600951212 /* log.c */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.c.c; name = log.c; path = src/log.c; sourceTree = ""; }; - 28715A1220B3E5780047F481 /* skolem_encodings.c */ = {isa = PBXFileReference; lastKnownFileType = sourcecode.c.c; name = skolem_encodings.c; path = src/skolem_encodings.c; sourceTree = ""; }; 287BB7C11E0609B000AAE180 /* partitions.c */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.c.c; name = partitions.c; path = src/partitions.c; sourceTree = ""; }; 287C3B0B1E37EF7B00F7096A /* examples.c */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.c.c; name = examples.c; path = src/examples.c; sourceTree = ""; }; 287C3B0C1E37EF7B00F7096A /* examples.h */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.c.h; name = examples.h; path = src/examples.h; sourceTree = ""; }; @@ -314,7 +312,6 @@ 28DA30F31DFFDD2600EABCA6 /* skolem_dependencies.h */, 28DA30F21DFFDD2600EABCA6 /* skolem_dependencies.c */, 28FEE64A1EDA304000A9D8CA /* skolem_conflict_analysis.c */, - 28715A1220B3E5780047F481 /* skolem_encodings.c */, ); name = skolem; sourceTree = ""; @@ -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 */, diff --git a/src/cadet2.c b/src/cadet2.c index 19bcb8e..de69a02 100644 --- a/src/cadet2.c +++ b/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); diff --git a/src/certify_SAT.c b/src/certify_SAT.c index 55e1322..1c62ec9 100644 --- a/src/certify_SAT.c +++ b/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,8 +471,7 @@ 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!"); + valid = cert_validate_quantifier_elimination(a, c2->qcnf, aigerlits, projection); } else { // Create function int_vector* out_aigerlits = int_vector_copy(aigerlits); @@ -493,18 +496,17 @@ 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!"); + 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); diff --git a/src/main.c b/src/main.c index b415266..6abdb29 100644 --- a/src/main.c +++ b/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) { diff --git a/src/options.c b/src/options.c index 4a516b3..1eaf6b3 100644 --- a/src/options.c +++ b/src/options.c @@ -66,7 +66,6 @@ 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 return o; diff --git a/src/options.h b/src/options.h index 0a8f87d..d16254b 100644 --- a/src/options.h +++ b/src/options.h @@ -28,7 +28,6 @@ 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; // Use a configuration of CADET 2 that is easier to debug than the diff --git a/src/satsolver_picosat_assumptions.c b/src/satsolver_picosat_assumptions.c index fdacb7a..06b753f 100644 --- a/src/satsolver_picosat_assumptions.c +++ b/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 } diff --git a/src/skolem.c b/src/skolem.c index 9eba2a8..bac884d 100644 --- a/src/skolem.c +++ b/src/skolem.c @@ -208,7 +208,6 @@ void skolem_new_variable(Skolem* s, unsigned var_id) { && !skolem_is_deterministic(s, var_id)) { skolem_update_deterministic(s, var_id); - skolem_update_depends_on_decision_satlit(s, var_id, - s->satlit_true); int innerlit = satsolver_inc_max_var(s->skolem); skolem_update_pos_lit(s, var_id, innerlit); @@ -679,8 +678,6 @@ void skolem_propagate_determinicity(Skolem* s, unsigned var_id) { skolem_add_clauses_using_existing_satlits(s, var_id, &v->pos_occs); skolem_add_clauses_using_existing_satlits(s, var_id, &v->neg_occs); - - skolem_encode_depends_on_decision(s, var_id); } else { // add clauses with unique consequence as partial function skolem_fix_lit_for_unique_antecedents(s, (Lit) (int) var_id, false); @@ -691,8 +688,6 @@ void skolem_propagate_determinicity(Skolem* s, unsigned var_id) { satsolver_add(s->skolem, skolem_get_satsolver_lit(s, - (Lit) var_id)); satsolver_clause_finished(s->skolem); - skolem_encode_depends_on_decision(s, var_id); - skolem_global_conflict_check(s, var_id); if (skolem_is_conflicted(s)) { return; @@ -753,7 +748,6 @@ 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)); - skolem_encode_depends_on_decision(s, var_id); } else { // pure and locally conflicted skolem_fix_lit_for_unique_antecedents(s, pure_polarity * (Lit) var_id, true); @@ -812,8 +806,6 @@ void skolem_propagate_pure_variable(Skolem* s, unsigned var_id) { satsolver_add(s->skolem, skolem_get_satsolver_lit(s, - (Lit) var_id)); satsolver_clause_finished(s->skolem); - skolem_encode_depends_on_decision(s, var_id); - skolem_global_conflict_check(s, var_id); if (skolem_is_conflicted(s)) { return; @@ -1165,12 +1157,6 @@ void skolem_undo(void* parent, char type, void* obj) { int_vector_pop(s->universals_assumptions); break; - 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); - break; - default: V0("Unknown undo operation in skolem.c: %d\n", (int) type); NOT_IMPLEMENTED(); @@ -1339,8 +1325,6 @@ void skolem_assign_constant_value(Skolem* s, Lit lit, union Dependencies propaga skolem_update_neg_lit(s, var_id, s->satlit_true); } - skolem_encode_depends_on_decision(s, var_id); - // Global conflict check! // This check may put s in conflict state; returns after this call. // Callee has to check for conflict state. @@ -1360,10 +1344,6 @@ void skolem_assign_constant_value(Skolem* s, Lit lit, union Dependencies propaga skolem_update_dependencies(s, var_id, propagation_deps); - if (!potentially_conflicted) { // otherwise it was already encoded above - skolem_encode_depends_on_decision(s, var_id); - } - // Queue potentially new constants vector* opp_occs = qcnf_get_occs_of_lit(s->qcnf, - lit); for (unsigned i = 0; i < vector_count(opp_occs); i++) { @@ -1483,8 +1463,7 @@ void skolem_decision(Skolem* s, Lit decision_lit) { * checked at the same time, and a later variable is determined to be conflicted even though for * the same input the decision var would be conflicted as well. */ - bool positive_side_needs_complete_definitions_too = s->options->functional_synthesis; - skolem_fix_lit_for_unique_antecedents(s, decision_lit, positive_side_needs_complete_definitions_too); + skolem_fix_lit_for_unique_antecedents(s, decision_lit, false); bool opposite_case_exists = skolem_fix_lit_for_unique_antecedents(s, - decision_lit, true); // Here we already fix the function domain decisions @@ -1543,9 +1522,6 @@ void skolem_decision(Skolem* s, Lit decision_lit) { satsolver_add(s->skolem, - val_satlit); satsolver_clause_finished(s->skolem); - - skolem_encode_depends_on_decision(s, decision_var_id); - // encode depends_on_decision_satlit // actual := old || (-val && -opposite) // onesided only: actual => (old || (-val && -opposite)) diff --git a/src/skolem.h b/src/skolem.h index 47bd100..002ca81 100644 --- a/src/skolem.h +++ b/src/skolem.h @@ -163,8 +163,8 @@ void skolem_add_potentially_conflicted(Skolem*, unsigned var_id); void skolem_print_debug_info(Skolem*); void skolem_print_statistics(Skolem*); void skolem_print_deterministic_vars(Skolem*); + // PRIVATE FUNCTIONS -void skolem_encode_depends_on_decision(Skolem* s, unsigned var_id); typedef enum { SKOLEM_OP_UPDATE_INFO_POS_LIT, // obj contains the variable and the previous poslit, see union skolem_undo_union @@ -182,8 +182,7 @@ typedef enum { SKOLEM_OP_POTENTIALLY_CONFLICTED_VAR, SKOLEM_OP_DECISION_LVL, SKOLEM_OP_DECISION, - SKOLEM_OP_UNIVERSAL_ASSUMPTION, - SKOLEM_OP_UPDATE_INFO_DEPENDS_ON_DECISION_SATLIT + SKOLEM_OP_UNIVERSAL_ASSUMPTION } SKOLEM_OP; void skolem_undo(void*,char,void*); diff --git a/src/skolem_encodings.c b/src/skolem_encodings.c deleted file mode 100644 index 615cba4..0000000 --- a/src/skolem_encodings.c +++ /dev/null @@ -1,196 +0,0 @@ -// -// skolem_encodings.c -// cadet -// -// Created by Markus Rabe on 21.05.18. -// Copyright © 2018 UC Berkeley. All rights reserved. -// - -#include "skolem.h" -#include "log.h" - -int skolem_encode_antecedent_satisfied(Skolem* s, Clause* c) { - Lit uc = skolem_get_unique_consequence(s, c); - assert(uc != 0); - if (c->size == 1) { - return s->satlit_true; - } - if (c->size == 2) { - for (unsigned i = 0; i < c->size; i++) { - Lit l = c->occs[i]; - if (l != uc) { - return skolem_get_satsolver_lit(s, -l); - } - } - } - for (unsigned i = 0; i < c->size; i++) { - Lit l = c->occs[i]; - if (l != uc && skolem_lit_satisfied(s, l)) { - return - s->satlit_true; - } - } - - int antecedent_satisfied = satsolver_inc_max_var(s->skolem); - - for (unsigned i = 0; i < c->size; i++) { - Lit l = c->occs[i]; - if (l != uc) { - int other_satlit = skolem_get_satsolver_lit(s, l); - satsolver_add(s->skolem, other_satlit); - } - } - satsolver_add(s->skolem, antecedent_satisfied); - satsolver_clause_finished(s->skolem); - - for (unsigned i = 0; i < c->size; i++) { - Lit l = c->occs[i]; - if (l != uc) { - int other_satlit = skolem_get_satsolver_lit(s, l); - satsolver_add(s->skolem, - other_satlit); - satsolver_add(s->skolem, - antecedent_satisfied); - satsolver_clause_finished(s->skolem); - } - } - - return antecedent_satisfied; -} - - -int skolem_encode_antecedent_inependently_satisfied(Skolem* s, Clause* c) { - int satisfied = skolem_encode_antecedent_satisfied(s, c); - if (satisfied == - s->satlit_true) { - return - s->satlit_true; - } - Lit uc = skolem_get_unique_consequence(s, c); - - // Check if any of the lit_depends are statically false; can avoid allocating a new satsolver var - for (unsigned i = 0; i < c->size; i++) { - Lit l = c->occs[i]; - unsigned v = lit_to_var(l); - if (l != uc) { - int lit_depends = skolem_get_depends_on_decision_satlit(s, v); - if (lit_depends == s->satlit_true) { - return - s->satlit_true; - } - } - } - - int antecedent_sat_and_indep = satsolver_inc_max_var(s->skolem); - - // sat_and_indep := satisfied && -(lit_depends || ... || lit_depends) - for (unsigned i = 0; i < c->size; i++) { - Lit l = c->occs[i]; - unsigned v = lit_to_var(l); - if (l != uc) { - int lit_depends = skolem_get_depends_on_decision_satlit(s, v); - satsolver_add(s->skolem, - lit_depends); - satsolver_add(s->skolem, - antecedent_sat_and_indep); - satsolver_clause_finished(s->skolem); - } - } - - satsolver_add(s->skolem, satisfied); - satsolver_add(s->skolem, - antecedent_sat_and_indep); - satsolver_clause_finished(s->skolem); - - for (unsigned i = 0; i < c->size; i++) { - Lit l = c->occs[i]; - unsigned v = lit_to_var(l); - if (l != uc) { - int lit_depends = skolem_get_depends_on_decision_satlit(s, v); - satsolver_add(s->skolem, lit_depends); - } - } - satsolver_add(s->skolem, - satisfied); - satsolver_add(s->skolem, antecedent_sat_and_indep); - satsolver_clause_finished(s->skolem); - - - V4("Antecedent of clause %u independently satsified satlit: %d\n", c->clause_idx, antecedent_sat_and_indep); - return antecedent_sat_and_indep; -} - -bool skolem_encode_lit_is_definitely_independent(Skolem* s, Lit lit) { - if (skolem_is_decision_var(s, lit_to_var(lit))) { - return false; - } - vector* occs = qcnf_get_occs_of_lit(s->qcnf, lit); - for (unsigned i = 0; i < vector_count(occs); i++) { - Clause* c = vector_get(occs, i); - Lit uc = skolem_get_unique_consequence(s, c); - if (uc == lit) { - for (unsigned i = 0; i < c->size; i++) { - Lit l = c->occs[i]; - unsigned v = lit_to_var(l); - if (l != uc) { - int lit_depends = skolem_get_depends_on_decision_satlit(s, v); - if (lit_depends != - s->satlit_true) { - return false; - } - } - } - } - } - return true; -} - -int skolem_encode_lit_satisfied_and_depends_on_decisions(Skolem* s, Lit lit) { - if (skolem_encode_lit_is_definitely_independent(s, lit)) { - return - s->satlit_true; - } - - int_vector* indep_lits = int_vector_init(); - vector* occs = qcnf_get_occs_of_lit(s->qcnf, lit); - for (unsigned i = 0; i < vector_count(occs); i++) { - Clause* c = vector_get(occs, i); - if (skolem_get_unique_consequence(s, c) == lit) { - int indep = skolem_encode_antecedent_inependently_satisfied(s, c); - int_vector_add(indep_lits, indep); - } - } - if (int_vector_count(indep_lits) == 0) { - int_vector_free(indep_lits); - return skolem_get_satsolver_lit(s, lit); - } - - int satlit_is_set_and_depends = satsolver_inc_max_var(s->skolem); - for (unsigned i = 0; i < int_vector_count(indep_lits); i++) { - int indep = int_vector_get(indep_lits, i); - satsolver_add(s->skolem, - indep); - satsolver_add(s->skolem, - satlit_is_set_and_depends); - satsolver_clause_finished(s->skolem); - } - satsolver_add(s->skolem, skolem_get_satsolver_lit(s, lit)); - satsolver_add(s->skolem, - satlit_is_set_and_depends); - satsolver_clause_finished(s->skolem); - - int_vector_free(indep_lits); - return satlit_is_set_and_depends; -} - - -void skolem_encode_depends_on_decision(Skolem* s, unsigned var_id) { - if (!s->options->functional_synthesis || qcnf_is_universal(s->qcnf, var_id)) { - return; - } - - int depends_pos = skolem_encode_lit_satisfied_and_depends_on_decisions(s, (Lit) var_id); - int depends_neg = skolem_encode_lit_satisfied_and_depends_on_decisions(s, - (Lit) var_id); - if (depends_neg == - s->satlit_true && depends_pos == - s->satlit_true) { - // no new cases can exist, so old_depends_satlit can remain - return; - } - - int old_depends_on_decision_satlit = skolem_get_depends_on_decision_satlit(s, var_id); - int new_depends_on_decision_satlit = satsolver_inc_max_var(s->skolem); - - // new => old | pos | neg - satsolver_add(s->skolem, depends_pos); - satsolver_add(s->skolem, depends_neg); - satsolver_add(s->skolem, old_depends_on_decision_satlit); - satsolver_add(s->skolem, - new_depends_on_decision_satlit); - satsolver_clause_finished(s->skolem); - - skolem_update_depends_on_decision_satlit(s, var_id, new_depends_on_decision_satlit); - -} diff --git a/src/skolem_var.c b/src/skolem_var.c index 34c34f5..dbeb452 100644 --- a/src/skolem_var.c +++ b/src/skolem_var.c @@ -282,19 +282,6 @@ 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(satlit != 0); - - V4("Setting depends_on_decision_satlit %d for var %u\n", satlit, var_id); - union skolem_undo_union suu; - suu.sus.var_id = var_id; - suu.sus.val = sv->depends_on_decision_satlit; - stack_push_op(s->stack, SKOLEM_OP_UPDATE_INFO_DEPENDS_ON_DECISION_SATLIT, suu.ptr); - sv->depends_on_decision_satlit = satlit; -} - void skolem_update_dependencies(Skolem* s, unsigned var_id, union Dependencies deps) { #ifdef DEBUG Var* v = var_vector_get(s->qcnf->vars, var_id); diff --git a/src/skolem_var.h b/src/skolem_var.h index a003a0a..9616869 100644 --- a/src/skolem_var.h +++ b/src/skolem_var.h @@ -59,7 +59,6 @@ void skolem_update_pure_pos(Skolem*, unsigned var_id, unsigned pos_lit); void skolem_update_pure_neg(Skolem*, unsigned var_id, unsigned pos_lit); void skolem_update_deterministic(Skolem*, unsigned var_id); void skolem_update_decision(Skolem*, Lit lit); -void skolem_update_depends_on_decision_satlit(Skolem*, unsigned var_id, int satlit); void skolem_update_dependencies(Skolem*, unsigned var_id, union Dependencies deps); void skolem_undo_dependencies(Skolem*, void* data); From d5c46c7536d8a647868199c050b082fefd6fef93 Mon Sep 17 00:00:00 2001 From: Markus N Rabe Date: Wed, 26 Dec 2018 21:06:00 +0100 Subject: [PATCH 2/7] fixed bug in functional synthesis due to outdated encoding in global conflict check --- src/cadet2.c | 2 +- src/skolem.c | 38 +++++--------------------------------- 2 files changed, 6 insertions(+), 34 deletions(-) diff --git a/src/cadet2.c b/src/cadet2.c index de69a02..ec112c6 100644 --- a/src/cadet2.c +++ b/src/cadet2.c @@ -833,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)); diff --git a/src/skolem.c b/src/skolem.c index bac884d..c1d0c56 100644 --- a/src/skolem.c +++ b/src/skolem.c @@ -26,8 +26,9 @@ Skolem* skolem_init(QCNF* qcnf, Options* o) { s->qcnf = qcnf; s->skolem = satsolver_init(); - +// satsolver_trace_commands(s->skolem); c2_trace_for_profiling_initialize(o, s->skolem); + s->state = SKOLEM_STATE_READY; s->decision_lvl = 0; @@ -932,39 +933,10 @@ void skolem_propagate_partial_over_clause_for_lit(Skolem* s, Clause* c, Lit lit, void skolem_encode_global_conflict_check(Skolem* s) { assert(int_vector_count(s->potentially_conflicted_variables) == int_vector_count(s->potential_conflicts_satlits)); - if (s->options->functional_synthesis) { - int_vector* disjunction = int_vector_init(); - for (unsigned i = 0; i < int_vector_count(s->potentially_conflicted_variables); i++) { - unsigned conflicted_var = (unsigned) int_vector_get(s->potentially_conflicted_variables, i); - - int is_necessary_conflict = satsolver_inc_max_var(s->skolem); - int_vector_add(disjunction, is_necessary_conflict); - - satsolver_add(s->skolem, int_vector_get(s->potential_conflicts_satlits, i)); - satsolver_add(s->skolem, - is_necessary_conflict); - satsolver_clause_finished(s->skolem); - - satsolver_add(s->skolem, skolem_get_depends_on_decision_satlit(s, conflicted_var)); - satsolver_add(s->skolem, - is_necessary_conflict); - satsolver_clause_finished(s->skolem); - } - for (unsigned i = 0; i < int_vector_count(disjunction); i++) { - int is_necessary_conflict = int_vector_get(disjunction, i); - satsolver_add(s->skolem, is_necessary_conflict); - } - satsolver_clause_finished(s->skolem); - int_vector_free(disjunction); - -// for (unsigned i = 0; i < int_vector_count(s->decision_satlits); i++) { -// satsolver_add(s->skolem, int_vector_get(s->decision_satlits, i)); -// } -// satsolver_clause_finished(s->skolem); - } else { - for (unsigned i = 0; i < int_vector_count(s->potential_conflicts_satlits); i++) { - satsolver_add(s->skolem, int_vector_get(s->potential_conflicts_satlits, i)); - } - satsolver_clause_finished(s->skolem); + for (unsigned i = 0; i < int_vector_count(s->potential_conflicts_satlits); i++) { + satsolver_add(s->skolem, int_vector_get(s->potential_conflicts_satlits, i)); } + satsolver_clause_finished(s->skolem); } unsigned skolem_global_conflict_check(Skolem* s, unsigned var_id) { From 71e25a2eb77a06af07d4f1687ba53798fbaae04a Mon Sep 17 00:00:00 2001 From: Markus N Rabe Date: Wed, 26 Dec 2018 21:52:21 +0100 Subject: [PATCH 3/7] removed deprecated flag from tester.py --- scripts/tester.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/tester.py b/scripts/tester.py index 123829a..669f0cd 100755 --- a/scripts/tester.py +++ b/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: From 6f8ad12bb3b07ecfd49b0e1d92053bad14cc9750 Mon Sep 17 00:00:00 2001 From: Markus N Rabe Date: Mon, 31 Dec 2018 11:23:58 -0800 Subject: [PATCH 4/7] updated functional synthesis paths in instances and fixed small problem in run.py with crashing runs --- integration-tests/instances.txt | 168 ++++++++++++++++---------------- scripts/run.py | 12 ++- 2 files changed, 92 insertions(+), 88 deletions(-) diff --git a/integration-tests/instances.txt b/integration-tests/instances.txt index 125a63c..37d56fa 100644 --- a/integration-tests/instances.txt +++ b/integration-tests/instances.txt @@ -6753,48 +6753,48 @@ integration-tests/test_unsat.qdimacs | 20 ../qbf-benchmarks/FV/sterin/qrevenge/adder-self-2QBF/adder-32-adder-32.qdimacs.gz | 20 [functional-synthesis] -../qbf-benchmarks/synthesis/akshay/functional-synthesis/arithmetic/ceiling32.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/arithmetic/ceiling128.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/arithmetic/ceiling256.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/arithmetic/decomposition32.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/arithmetic/decomposition128.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/arithmetic/decomposition256.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/arithmetic/equalization32.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/arithmetic/equalization128.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/arithmetic/equalization256.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/arithmetic/floor32.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/arithmetic/floor128.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/arithmetic/floor256.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/arithmetic/intermediate32.qdimacs.gz | 30 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/arithmetic/intermediate128.qdimacs.gz | 30 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/arithmetic/intermediate256.qdimacs.gz | 30 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/bobsm5378d2_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/bobsm9234_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/bobsmcodic_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/bobsmfpu_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/bobsmhdlc_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/bobsmhdlc1_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/bobsmhdlc2_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/bobsmhdlc3_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/bobtuint31neg_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/eijkbs1512_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/eijkbs3330_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/eijkbs4863_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/kenflashp01_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/kenflashp02_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/kenflashp04_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/kenflashp12_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/kenoopp1_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/neclaftp2001_all_bit_differing_from_cycle.qdimacs.gz | 20 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/neclaftp2002_all_bit_differing_from_cycle.qdimacs.gz | 20 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/neclaftp3001_all_bit_differing_from_cycle.qdimacs.gz | 20 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/neclaftp4001_all_bit_differing_from_cycle.qdimacs.gz | 20 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/neclaftp4002_all_bit_differing_from_cycle.qdimacs.gz | 20 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/pdtpmsgigamax_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/pdtpmsmiim_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/pdtpmsns3_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/pdtpmsrotate32_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/pdtpmssfeistel_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/arithmetic/ceiling32.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/arithmetic/ceiling128.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/arithmetic/ceiling256.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/arithmetic/decomposition32.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/arithmetic/decomposition128.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/arithmetic/decomposition256.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/arithmetic/equalization32.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/arithmetic/equalization128.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/arithmetic/equalization256.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/arithmetic/floor32.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/arithmetic/floor128.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/arithmetic/floor256.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/arithmetic/intermediate32.qdimacs.gz | 30 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/arithmetic/intermediate128.qdimacs.gz | 30 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/arithmetic/intermediate256.qdimacs.gz | 30 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/bobsm5378d2_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/bobsm9234_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/bobsmcodic_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/bobsmfpu_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/bobsmhdlc_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/bobsmhdlc1_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/bobsmhdlc2_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/bobsmhdlc3_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/bobtuint31neg_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/eijkbs1512_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/eijkbs3330_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/eijkbs4863_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/kenflashp01_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/kenflashp02_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/kenflashp04_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/kenflashp12_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/kenoopp1_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/neclaftp2001_all_bit_differing_from_cycle.qdimacs.gz | 20 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/neclaftp2002_all_bit_differing_from_cycle.qdimacs.gz | 20 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/neclaftp3001_all_bit_differing_from_cycle.qdimacs.gz | 20 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/neclaftp4001_all_bit_differing_from_cycle.qdimacs.gz | 20 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/neclaftp4002_all_bit_differing_from_cycle.qdimacs.gz | 20 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/pdtpmsgigamax_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/pdtpmsmiim_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/pdtpmsns3_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/pdtpmsrotate32_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/pdtpmssfeistel_all_bit_differing_from_cycle.qdimacs.gz | 10 [qbfeval2017-2QBF] @@ -7198,48 +7198,48 @@ integration-tests/test_unsat.qdimacs | 20 ../qbf-benchmarks/evaluations/qbflib2010-2QBF/qshifter_7.qdimacs.gz | 10 ../qbf-benchmarks/evaluations/qbflib2010-2QBF/qshifter_8.qdimacs.gz | 10 ../qbf-benchmarks/evaluations/qbfeval2017-2QBF/kenflashp04.qdimacs.gz | 30 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/arithmetic/ceiling32.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/arithmetic/ceiling128.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/arithmetic/ceiling256.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/arithmetic/decomposition32.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/arithmetic/decomposition128.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/arithmetic/decomposition256.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/arithmetic/equalization32.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/arithmetic/equalization128.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/arithmetic/equalization256.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/arithmetic/floor32.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/arithmetic/floor128.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/arithmetic/floor256.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/arithmetic/intermediate32.qdimacs.gz | 30 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/arithmetic/intermediate128.qdimacs.gz | 30 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/arithmetic/intermediate256.qdimacs.gz | 30 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/bobsm5378d2_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/bobsm9234_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/bobsmcodic_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/bobsmfpu_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/bobsmhdlc_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/bobsmhdlc1_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/bobsmhdlc2_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/bobsmhdlc3_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/bobtuint31neg_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/eijkbs1512_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/eijkbs3330_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/eijkbs4863_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/kenflashp01_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/kenflashp02_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/kenflashp04_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/kenflashp12_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/kenoopp1_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/neclaftp2001_all_bit_differing_from_cycle.qdimacs.gz | 20 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/neclaftp2002_all_bit_differing_from_cycle.qdimacs.gz | 20 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/neclaftp3001_all_bit_differing_from_cycle.qdimacs.gz | 20 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/neclaftp4001_all_bit_differing_from_cycle.qdimacs.gz | 20 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/neclaftp4002_all_bit_differing_from_cycle.qdimacs.gz | 20 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/pdtpmsgigamax_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/pdtpmsmiim_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/pdtpmsns3_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/pdtpmsrotate32_all_bit_differing_from_cycle.qdimacs.gz | 10 -../qbf-benchmarks/synthesis/akshay/functional-synthesis/disjunctive_decomposition/pdtpmssfeistel_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/arithmetic/ceiling32.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/arithmetic/ceiling128.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/arithmetic/ceiling256.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/arithmetic/decomposition32.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/arithmetic/decomposition128.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/arithmetic/decomposition256.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/arithmetic/equalization32.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/arithmetic/equalization128.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/arithmetic/equalization256.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/arithmetic/floor32.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/arithmetic/floor128.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/arithmetic/floor256.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/arithmetic/intermediate32.qdimacs.gz | 30 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/arithmetic/intermediate128.qdimacs.gz | 30 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/arithmetic/intermediate256.qdimacs.gz | 30 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/bobsm5378d2_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/bobsm9234_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/bobsmcodic_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/bobsmfpu_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/bobsmhdlc_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/bobsmhdlc1_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/bobsmhdlc2_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/bobsmhdlc3_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/bobtuint31neg_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/eijkbs1512_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/eijkbs3330_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/eijkbs4863_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/kenflashp01_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/kenflashp02_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/kenflashp04_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/kenflashp12_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/kenoopp1_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/neclaftp2001_all_bit_differing_from_cycle.qdimacs.gz | 20 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/neclaftp2002_all_bit_differing_from_cycle.qdimacs.gz | 20 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/neclaftp3001_all_bit_differing_from_cycle.qdimacs.gz | 20 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/neclaftp4001_all_bit_differing_from_cycle.qdimacs.gz | 20 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/neclaftp4002_all_bit_differing_from_cycle.qdimacs.gz | 20 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/pdtpmsgigamax_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/pdtpmsmiim_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/pdtpmsns3_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/pdtpmsrotate32_all_bit_differing_from_cycle.qdimacs.gz | 10 +../qbf-benchmarks/functional-synthesis/akshay/functional-synthesis/disjunctive_decomposition/pdtpmssfeistel_all_bit_differing_from_cycle.qdimacs.gz | 10 ../qbf-benchmarks/evaluations/qbfeval2017-2QBF/ctrl.e#1.a#3.E#110.A#48.c#.w#9.s#13.asp.qdimacs.gz | 30 ../qbf-benchmarks/evaluations/qbfeval2017-2QBF/ctrl.e#1.a#3.E#118.A#48.c#.w#5.s#7.asp.qdimacs.gz | 30 ../qbf-benchmarks/evaluations/qbfeval2017-2QBF/ctrl.e#1.a#3.E#128.A#48.c#.w#5.s#1.asp.qdimacs.gz | 30 diff --git a/scripts/run.py b/scripts/run.py index ca0f43a..47eecd5 100755 --- a/scripts/run.py +++ b/scripts/run.py @@ -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: From 1843f137a96592d4f77c3aab3e2b66b20205a400 Mon Sep 17 00:00:00 2001 From: Markus N Rabe Date: Fri, 4 Jan 2019 09:09:07 -0800 Subject: [PATCH 5/7] added --dontverify option --- src/certify_SAT.c | 11 ++++++++--- src/main.c | 2 ++ src/options.c | 5 +++-- src/options.h | 1 + 4 files changed, 14 insertions(+), 5 deletions(-) diff --git a/src/certify_SAT.c b/src/certify_SAT.c index 1c62ec9..1ba3824 100644 --- a/src/certify_SAT.c +++ b/src/certify_SAT.c @@ -471,8 +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); - valid = cert_validate_quantifier_elimination(a, c2->qcnf, aigerlits, projection); - + 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++) { @@ -495,7 +498,9 @@ void c2_write_AIG_certificate(C2* c2) { cert_define_aiger_outputs(skolem_dlvl0, a, out_aigerlits); - if (!c2->options->functional_synthesis) { + 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 { valid = cert_validate_functional_synthesis(a, c2->qcnf, out_aigerlits, case_selectors); diff --git a/src/main.c b/src/main.c index 6abdb29..f3249e3 100644 --- a/src/main.c +++ b/src/main.c @@ -192,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]); diff --git a/src/options.c b/src/options.c index 1eaf6b3..b55e8d5 100644 --- a/src/options.c +++ b/src/options.c @@ -67,7 +67,7 @@ Options* default_options() { o->rl_slim_state = false; o->reinforcement_learning_mock = false; o->hard_decision_limit = 0; // 0 means no limit - + o->verify = 1; return o; } @@ -113,7 +113,8 @@ char* options_get_help() { "\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" "\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" + "\t--dontverify\t\tDo not verify results.\n" "\n", debug_verbosity, o->reinforcement_learning, diff --git a/src/options.h b/src/options.h index d16254b..67f8b22 100644 --- a/src/options.h +++ b/src/options.h @@ -29,6 +29,7 @@ typedef struct { bool rl_slim_state; bool reinforcement_learning_mock; // for testing reinforcement learning code unsigned hard_decision_limit; + bool verify; // Use a configuration of CADET 2 that is easier to debug than the // performance-oriented configuration From 2bcf0e005ed9b2a692cd90f54f57b56dc8f5e8df Mon Sep 17 00:00:00 2001 From: Markus N Rabe Date: Fri, 4 Jan 2019 14:01:47 -0800 Subject: [PATCH 6/7] fixed help output --- src/options.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/options.c b/src/options.c index b55e8d5..ffb9184 100644 --- a/src/options.c +++ b/src/options.c @@ -112,9 +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--dontverify\t\tDo not verify results.\n" "\n", debug_verbosity, o->reinforcement_learning, From 6151c480150abda5c4181ddd1df3768b87b67db3 Mon Sep 17 00:00:00 2001 From: Markus N Rabe Date: Sat, 16 Mar 2019 11:21:52 -0700 Subject: [PATCH 7/7] improved run.py --- scripts/run.py | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/scripts/run.py b/scripts/run.py index 47eecd5..266fbca 100755 --- a/scripts/run.py +++ b/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