diff --git a/LICENSE b/LICENSE index 81065ffc..a6c4b721 100644 --- a/LICENSE +++ b/LICENSE @@ -2,6 +2,7 @@ MIT License Copyright (c) 2016-2021 Armin Biere, Johannes Kepler University Linz, Austria Copyright (c) 2020-2021 Mathias Fleury, Johannes Kepler University Linz, Austria +Copyright (c) 2020-2021 Nils Froleyks, Johannes Kepler University Linz, Austria Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal diff --git a/NEWS.md b/NEWS.md new file mode 100644 index 00000000..797dc2db --- /dev/null +++ b/NEWS.md @@ -0,0 +1,10 @@ +Version 1.5.0 +------------- + +- added constrain interface to optimize use with IC3 + +Version 1.4.2 +------------- + +- replaced "`while () push_back ()`" with "`if () resize ()`" idiom + (thanks go to Alexander Smal for pointing this out) diff --git a/VERSION b/VERSION index 347f5833..bc80560f 100644 --- a/VERSION +++ b/VERSION @@ -1 +1 @@ -1.4.1 +1.5.0 diff --git a/src/assume.cpp b/src/assume.cpp index c79cfa80..4e1ed8ac 100644 --- a/src/assume.cpp +++ b/src/assume.cpp @@ -31,135 +31,180 @@ void Internal::failing () { assert (analyzed.empty ()); assert (clause.empty ()); - int first = 0; - - // Try to find two clashing assumptions. - // - for (auto & lit : assumptions) { - if (!assumed (-lit)) continue; - first = lit; - break; - } - - if (first) { - - // TODO: if 'first' is on the root-level, then, as below, we probably - // want an empty core. - - clause.push_back (first); - clause.push_back (-first); - - Flags & f = flags (first); + if (!unsat_constraint) { + // Search for failing assumptions in the (internal) assumption stack. - unsigned bit = bign (first); - assert (!(f.failed & bit)); - f.failed |= bit; - bit = bign (-first); - f.failed |= bit; + // There are in essence three cases: (1) An assumption is falsified on the + // root-level and then 'failed_unit' is set to that assumption, (2) two + // clashing assumptions are assumed and then 'failed_clashing' is set to + // the second assumed one, or otherwise (3) there is a failing assumption + // 'first_failed' with minimum (non-zero) decision level 'failed_level'. - } else { + int failed_unit = 0; + int failed_clashing = 0; + int first_failed = 0; + int failed_level = INT_MAX; - // Find an assumption falsified at smallest decision level. - // for (auto & lit : assumptions) { - const signed char tmp = val (lit); - if (tmp >= 0) continue; - if (!first || var (first).level > var (lit).level) - first = lit; + if (val (lit) >= 0) continue; + const Var & v = var (lit); + if (!v.level) { + failed_unit = lit; + break; + } + if (failed_clashing) continue; + if (!v.reason) failed_clashing = lit; + else if (!first_failed || v.level < failed_level) { + first_failed = lit; + failed_level = v.level; + } } - assert (first); - LOG ("starting with assumption %d falsified on decision level %d", - first, var (first).level); - - if (!var (first).level) { - - // TODO: I think marking this should yield an empty core - // and not mark 'first' as failed (similarly above). + // Get the 'failed' assumption from one of the three cases. + int failed; + if (failed_unit) + failed = failed_unit; + else if (failed_clashing) + failed = failed_clashing; + else + failed = first_failed; + assert (failed); + + // In any case mark literal 'failed' as failed assumption. + { + Flags & f = flags (failed); + const unsigned bit = bign (failed); + assert (!(f.failed & bit)); + f.failed |= bit; + } - LOG ("failed assumption %d", first); - clause.push_back (-first); + // First case (1). + if (failed_unit) { + assert (failed == failed_unit); + LOG ("root-level falsified assumption %d", failed); + goto DONE; + } - Flags & f = flags (first); - const unsigned bit = bign (first); + // Second case (2). + if (failed_clashing) { + assert (failed == failed_clashing); + LOG ("clashing assumptions %d and %d", failed, -failed); + Flags & f = flags (-failed); + const unsigned bit = bign (-failed); assert (!(f.failed & bit)); f.failed |= bit; + goto DONE; + } - } else { - - // The 'analyzed' stack serves as working stack for a BFS through the - // implication graph until decisions, which are all assumptions, or units - // are reached. This is simpler than corresponding code in 'analyze'. + // Fall through to third case (3). + LOG ("starting with assumption %d falsified on minimum decision level %d", + first_failed, failed_level); + + assert (first_failed); + assert (failed_level > 0); + + // The 'analyzed' stack serves as working stack for a BFS through the + // implication graph until decisions, which are all assumptions, or units + // are reached. This is simpler than corresponding code in 'analyze'. + { + LOG ("failed assumption %d", first_failed); + Flags & f = flags (first_failed); + assert (!f.seen); + f.seen = true; + assert (f.failed & bign (first_failed)); + analyzed.push_back (-first_failed); + clause.push_back (-first_failed); + } + } else { // unsat_constraint + // The assumptions necessary to fail each literal in the constraint are + // collected. + for (auto lit : constraint) { + lit *= -1; + assert (lit != INT_MIN); + flags (lit).seen = true; + analyzed.push_back (lit); + } + } - { - LOG ("failed assumption %d", first); - Flags & f = flags (first); - const unsigned bit = bign (first); + { + size_t next = 0; + + while (next < analyzed.size ()) { + const int lit = analyzed[next++]; + assert (val (lit) > 0); + Var & v = var (lit); + if (!v.level) continue; + + if (v.reason) { + assert (v.level); + LOG (v.reason, "analyze reason"); + for (const auto & other : *v.reason) { + Flags & f = flags (other); + if (f.seen) continue; + f.seen = true; + assert (val (other) < 0); + analyzed.push_back (-other); + } + } else { + assert (assumed (lit)); + LOG ("failed assumption %d", lit); + clause.push_back (-lit); + Flags & f = flags (lit); + const unsigned bit = bign (lit); assert (!(f.failed & bit)); f.failed |= bit; - f.seen = true; } + } + clear_analyzed_literals (); + + // TODO: We can not do clause minimization here, right? - analyzed.push_back (first); - clause.push_back (-first); - - size_t next = 0; - - while (next < analyzed.size ()) { - const int lit = analyzed[next++]; -#ifndef NDEBUG - if (first == lit) assert (val (lit) < 0); - else assert (val (lit) > 0); -#endif - Var & v = var (lit); - if (!v.level) continue; - - if (v.reason) { - assert (v.level); - LOG (v.reason, "analyze reason"); - for (const auto & other : *v.reason) { - Flags & f = flags (other); - if (f.seen) continue; - f.seen = true; - assert (val (other) < 0); - analyzed.push_back (-other); - } - } else { - assert (assumed (lit)); - LOG ("failed assumption %d", lit); - clause.push_back (-lit); - Flags & f = flags (lit); - const unsigned bit = bign (lit); - assert (!(f.failed & bit)); - f.failed |= bit; + VERBOSE (1, "found %zd failed assumptions %.0f%%", + clause.size (), percent (clause.size (), assumptions.size ())); + + // We do not actually need to learn this clause, since the conflict is + // forced already by some other clauses. There is also no bumping + // of variables nor clauses necessary. But we still want to check + // correctness of the claim that the determined subset of failing + // assumptions are a high-level core or equivalently their negations form + // a unit-implied clause. + // + if (!unsat_constraint) { + external->check_learned_clause (); + if (proof) { + proof->add_derived_clause(clause); + proof->delete_clause(clause); + } + } else { + for (auto lit : constraint) { + clause.push_back(-lit); + external->check_learned_clause (); + if (proof) { + proof->add_derived_clause(clause); + proof->delete_clause(clause); } + clause.pop_back(); } - clear_analyzed_literals (); - - // TODO, we can not do clause minimization here, right? } - } - VERBOSE (1, "found %zd failed assumptions %.0f%%", - clause.size (), percent (clause.size (), assumptions.size ())); - - // We do not actually need to learn this clause, since the conflict is - // forced already by some other clauses. There is also no bumping - // of variables nor clauses necessary. But we still want to check - // correctness of the claim that the determined subset of failing - // assumptions are a high-level core or equivalently their negations form - // a unit-implied clause. - // - external->check_learned_clause (); - if (proof) { - proof->add_derived_clause (clause); - proof->delete_clause (clause); + clause.clear (); } - clause.clear (); + +DONE: STOP (analyze); } +bool Internal::failed (int lit) { + if (!marked_failed) { + failing (); + marked_failed = true; + } + Flags &f = flags (lit); + const unsigned bit = bign (lit); + return (f.failed & bit) != 0; +} + // Add the start of each incremental phase (leaving the state // 'UNSATISFIABLE' actually) we reset all assumptions. @@ -173,6 +218,7 @@ void Internal::reset_assumptions () { } LOG ("cleared %zd assumptions", assumptions.size ()); assumptions.clear (); + marked_failed = true; } } diff --git a/src/bins.cpp b/src/bins.cpp index 8f108a33..03eb736e 100644 --- a/src/bins.cpp +++ b/src/bins.cpp @@ -8,8 +8,8 @@ namespace CaDiCaL { void Internal::init_bins () { assert (big.empty ()); - while (big.size () < 2*vsize) - big.push_back (Bins ()); + if (big.size () < 2*vsize) + big.resize (2*vsize, Bins ()); LOG ("initialized binary implication graph"); } diff --git a/src/cadical.hpp b/src/cadical.hpp index cbb064b9..cbe476d3 100644 --- a/src/cadical.hpp +++ b/src/cadical.hpp @@ -133,13 +133,13 @@ namespace CaDiCaL { // terminate (asynchronously) // SOLVING -------------------------> UNKNOWN // -// The important behaviour to remember is that adding or assuming a literal -// (immediately) destroys the satisfying assignment in the 'SATISFIED' state -// and vice versa resets all assumptions in the 'UNSATISFIED' state. This +// The important behaviour to remember is that adding, assuming or constraining +// a literal (immediately) destroys the satisfying assignment in the 'SATISFIED' +// state and vice versa resets all assumptions in the 'UNSATISFIED' state. This // is exactly the behaviour required by the IPASIR interface. // // Furthermore, the model can only be queried through 'val' in the -// 'SATISFIED' state, while extracting failed assumptions with 'val' only in +// 'SATISFIED' state, while extracting failed assumptions with 'failed' only in // the 'UNSATISFIED' state. Solving can only be started in the 'UNKNOWN' or // 'CONFIGURING' state or after the previous call to 'solve' yielded an // 'UNKNOWN, 'SATISFIED' or 'UNSATISFIED' state. @@ -286,6 +286,30 @@ class Solver { // ====== END IPASIR ===================================================== + //------------------------------------------------------------------------ + // Adds a literal to the constraint clause. Same functionality as 'add' but + // the clause only exists for the next call to solve (same lifetime as + // assumptions). Only one constraint may exists at a time. A new constraint + // replaces the old. + // The main application of this functonality is the model checking algorithm + // IC3. See our FMCAD'21 paper [FroleyksBiere-FMCAD'19] for more details. + // + // Add valid literal to the constraint clause or zero to terminate it. + // + // require (VALID) // recall 'VALID = READY | ADDING' + // if (lit) ensure (ADDING) // and thus VALID but not READY + // if (!lit) && !adding_clause ensure (UNKNOWN) // and thus READY + // + void constrain (int lit); + + // Determine whether the constraint was used to proof the unsatisfiability. + // Note that the formula might still be unsatisfiable without the constraint. + // + // require (UNSATISFIED) + // ensure (UNSATISFIED) + // + bool constraint_failed (); + //------------------------------------------------------------------------ // This function determines a good splitting literal. The result can be // zero if the formula is proven to be satisfiable or unsatisfiable. This @@ -305,7 +329,8 @@ class Solver { CubesWithStatus generate_cubes(int, int min_depth = 0); - void reset_assumptions(); + void reset_assumptions (); + void reset_constraint (); // Return the current state of the solver as defined above. // @@ -684,6 +709,11 @@ class Solver { //==== start of state ==================================================== + // The solver is in the state ADDING if either the current clause or the + // constraint (or both) is not yet terminated. + bool adding_clause; + bool adding_constraint; + State _state; // API states as discussed above. /*----------------------------------------------------------------------*/ diff --git a/src/ccadical.cpp b/src/ccadical.cpp index 2141c56a..e6e7d283 100644 --- a/src/ccadical.cpp +++ b/src/ccadical.cpp @@ -79,6 +79,14 @@ void ccadical_release (CCaDiCaL * wrapper) { delete (Wrapper*) wrapper; } +void ccadical_constrain (CCaDiCaL *wrapper, int lit){ + ((Wrapper*) wrapper)->solver->constrain (lit); +} + +int ccadical_constraint_failed (CCaDiCaL * wrapper) { + return ((Wrapper*) wrapper)->solver->constraint_failed (); +} + void ccadical_set_option (CCaDiCaL * wrapper, const char * name, int val) { ((Wrapper*) wrapper)->solver->set (name, val); diff --git a/src/ccadical.h b/src/ccadical.h index 4173aedc..332f842d 100644 --- a/src/ccadical.h +++ b/src/ccadical.h @@ -33,6 +33,8 @@ void ccadical_set_learn (CCaDiCaL *, // Non-IPASIR conformant 'C' functions. +void ccadical_constrain (CCaDiCaL *, int lit); +int ccadical_constraint_failed (CCaDiCaL *); void ccadical_set_option (CCaDiCaL *, const char * name, int val); void ccadical_limit (CCaDiCaL *, const char * name, int limit); int ccadical_get_option (CCaDiCaL *, const char * name); diff --git a/src/compact.cpp b/src/compact.cpp index 5598b239..386cad20 100644 --- a/src/compact.cpp +++ b/src/compact.cpp @@ -187,6 +187,13 @@ void Internal::compact () { reset_assumptions (); } + const bool is_constraint = !constraint.empty (); + if (is_constraint) { + assert (!external->constraint.empty ()); + LOG ("temporarily reset internal constraint"); + reset_constraint (); + } + /*======================================================================*/ // In this first part we only map stuff without reallocation / shrinking. /*======================================================================*/ @@ -321,6 +328,25 @@ void Internal::compact () { vals = new_vals; } + // 'constrain' uses 'val', so this code has to be after remapping that + if (is_constraint) { + assert (!level); + assert (!external->constraint.back ()); + for (auto elit : external->constraint){ + assert (elit != INT_MIN); + int eidx = abs (elit); + assert (eidx <= external->max_var); + int ilit = external->e2i[eidx]; + assert (!ilit == !elit); + if (elit < 0) + ilit = -ilit; + LOG ("re adding lit extrenal %d internal %d to constraint", elit, ilit); + constrain (ilit); + } + PHASE ("compact", stats.compacts, "added %zd external literals to constraint", + external->constraint.size () - 1); + } + mapper.map_vector (i2e); mapper.map2_vector (ptab); mapper.map_vector (btab); @@ -357,7 +383,7 @@ void Internal::compact () { } mapper.map_vector (stab); if (!saved.empty ()) { - for (const auto & idx : saved) + for (const auto idx : saved) scores.push_back (idx); scores.shrink (); } diff --git a/src/constrain.cpp b/src/constrain.cpp new file mode 100644 index 00000000..5713514c --- /dev/null +++ b/src/constrain.cpp @@ -0,0 +1,54 @@ +#include "internal.hpp" + +namespace CaDiCaL { + +void Internal::constrain (int lit) { + if (lit) constraint.push_back (lit); + else { + if (level) backtrack (); + LOG (constraint, "shrinking constraint"); + bool satisfied_constraint = false; + const vector::const_iterator end = constraint.end (); + vector::iterator i = constraint.begin (); + for (vector::const_iterator j = i; j != end; j++) { + int tmp = marked (*j); + if (tmp > 0) { + LOG ("removing duplicated literal %d from constraint", *j); + } else if (tmp < 0) { + LOG ("tautological since both %d and %d occur in constraint", -*j, *j); + satisfied_constraint = true; + break; + } else { + tmp = val (*j); + if (tmp < 0) { + LOG ("removing falsified literal %d from constraint clause", *j); + } else if (tmp > 0) { + LOG ("satisfied constraint with literal %d", *j); + satisfied_constraint = true; + break; + } else { + *i++ = *j; + mark (*j); + } + } + } + constraint.resize (i - constraint.begin ()); + for (const auto &lit : constraint) unmark (lit); + if (satisfied_constraint) constraint.clear (); + else if (constraint.empty ()) unsat_constraint = true; + else for (const auto lit : constraint) freeze (lit); + } +} + +bool Internal::failed_constraint () { + return unsat_constraint; +} + +void Internal::reset_constraint () { + for (auto lit : constraint) melt (lit); + LOG ("cleared %zd constraint literals", constraint.size ()); + constraint.clear (); + unsat_constraint = false; +} + +} diff --git a/src/decide.cpp b/src/decide.cpp index c7a6e636..1aa4b037 100644 --- a/src/decide.cpp +++ b/src/decide.cpp @@ -55,7 +55,7 @@ int Internal::decide_phase (int idx, bool target) { if (!phase && target) phase = phases.target[idx]; if (!phase) phase = phases.saved[idx]; - // The following should no be necessary and in some version we had even + // The following should not be necessary and in some version we had even // a hard 'COVER' assertion here to check for this. Unfortunately it // triggered for some users and we could not get to the root cause of // 'phase' still not being set here. The logic for phase and target @@ -79,7 +79,7 @@ int Internal::likely_phase (int idx) { return decide_phase (idx, false); } bool Internal::satisfied () { size_t assigned = trail.size (); if (propagated < assigned) return false; - if ((size_t) level < assumptions.size ()) return false; + if ((size_t) level < assumptions.size () + (!!constraint.size ())) return false; return (assigned == (size_t) max_var); } @@ -96,7 +96,6 @@ int Internal::decide () { const signed char tmp = val (lit); if (tmp < 0) { LOG ("assumption %d falsified", lit); - failing (); res = 20; } else if (tmp > 0) { LOG ("assumption %d already satisfied", lit); @@ -107,6 +106,33 @@ int Internal::decide () { LOG ("deciding assumption %d", lit); search_assume_decision (lit); } + } else if ((size_t) level == assumptions.size () && constraint.size ()) { + bool satisfied_constraint = false; + int unassigned_lit = 0; + for (const auto lit : constraint) { + const signed char tmp = val (lit); + if (tmp < 0) { + LOG ("constraint lit %d falsified", lit); + } else if (tmp > 0) { + LOG ("literal %d satisfies constraint and is implied by assumptions", lit); + level++; + control.push_back (Level (0, trail.size ())); + LOG ("added pseudo decision level for constraint"); + satisfied_constraint = true; + break; + } else if (!unassigned_lit) + unassigned_lit = lit; + } + if (!satisfied_constraint) { + if (unassigned_lit) { + LOG ("deciding %d to satisfy constraint", unassigned_lit); + search_assume_decision (unassigned_lit); + } else { + LOG ("failing constraint"); + unsat_constraint = true; + res = 20; + } + } } else { stats.decisions++; int idx = next_decision_variable (); @@ -114,6 +140,7 @@ int Internal::decide () { int decision = decide_phase (idx, target); search_assume_decision (decision); } + if (res) marked_failed = false; STOP (decide); return res; } diff --git a/src/ema.cpp b/src/ema.cpp index c61efbd8..5f09a3e8 100644 --- a/src/ema.cpp +++ b/src/ema.cpp @@ -21,9 +21,9 @@ namespace CaDiCaL { // // This old method is better than the initializations described in our // [BiereFroehlich-POS'15] paper and actually faster than the ADAM method, -// but less precise. This old method, which we consider obsolete but it -// could still be useful for implementations relying on integers instead of -// floating points thus only needs shifts and integer arithmetic. +// but less precise. We consider this old method obsolete now but it +// could still be useful for implementations relying on integers instead +// of floating points because it only needs shifts and integer arithmetic. // // Our new method for unbiased initialization of the exponential averages // works as follows. First the biased moving average is computed as usual. diff --git a/src/extend.cpp b/src/extend.cpp index d84ba95a..c08a19ac 100644 --- a/src/extend.cpp +++ b/src/extend.cpp @@ -105,8 +105,8 @@ void External::extend () { for (unsigned i = 1; i <= (unsigned) max_var; i++) { const int ilit = e2i[i]; if (!ilit) continue; - while (i >= vals.size ()) - vals.push_back (false); + if (i >= vals.size ()) + vals.resize (i + 1, false); vals[i] = (internal->val (ilit) > 0); updated++; } @@ -138,9 +138,9 @@ void External::extend () { LOG ("flipping blocking literal %d", lit); assert (lit); assert (lit != INT_MIN); - int idx = abs (lit); - while ((size_t) idx >= vals.size ()) - vals.push_back (false); + size_t idx = abs (lit); + if (idx >= vals.size ()) + vals.resize (idx + 1, false); vals[idx] = !vals[idx]; internal->stats.extended++; flipped++; diff --git a/src/external.cpp b/src/external.cpp index 73725d70..2bb8d92f 100644 --- a/src/external.cpp +++ b/src/external.cpp @@ -62,8 +62,8 @@ void External::init (int new_max_var) { assert (e2i[eidx] == (int) iidx); } if (internal->opts.checkfrozen) - while (new_max_var >= (int64_t) moltentab.size ()) - moltentab.push_back (false); + if (new_max_var >= (int64_t) moltentab.size ()) + moltentab.resize (1 + (size_t) new_max_var, false); assert (iidx == (size_t) new_internal_max_var + 1); assert (eidx == (size_t) new_max_var + 1); max_var = new_max_var; @@ -76,6 +76,11 @@ void External::reset_assumptions () { internal->reset_assumptions (); } +void External::reset_constraint () { + constraint.clear (); + internal->reset_constraint (); +} + void External::reset_extended () { if (!extended) return; LOG ("reset extended"); @@ -159,6 +164,24 @@ bool External::failed (int elit) { return internal->failed (ilit); } +void External::constrain (int elit) { + if (constraint.size () && !constraint.back ()) { + LOG (constraint, "replacing previous constraint"); + reset_constraint (); + } + assert (elit != INT_MIN); + reset_extended (); + constraint.push_back (elit); + const int ilit = internalize (elit); + assert (!elit == !ilit); + if (elit) LOG ("adding external %d as internal %d to constraint", elit, ilit); + internal->constrain (ilit); +} + +bool External::failed_constraint () { + return internal->failed_constraint (); +} + void External::phase (int elit) { assert (elit); assert (elit != INT_MIN); @@ -187,18 +210,22 @@ void External::unphase (int elit) { void External::check_satisfiable () { LOG ("checking satisfiable"); + if (!extended) extend (); if (internal->opts.checkwitness) check_assignment (&External::ival); if (internal->opts.checkassumptions && !assumptions.empty ()) check_assumptions_satisfied (); + if (internal->opts.checkconstraint && !constraint.empty ()) + check_constraint_satisfied (); } // Internal checker if 'solve' claims formula to be unsatisfiable. void External::check_unsatisfiable () { LOG ("checking unsatisfiable"); - if (internal->opts.checkfailed && !assumptions.empty ()) - check_assumptions_failing (); + if (!internal->opts.checkfailed) return; + if (!assumptions.empty () || !constraint.empty ()) + check_failing (); } // Check result of 'solve' to be correct. @@ -239,7 +266,6 @@ int External::solve (bool preprocess_only) { reset_extended (); update_molten_literals (); int res = internal->solve (preprocess_only); - if (res == 10) extend (); check_solve_result (res); reset_limits (); return res; @@ -282,8 +308,8 @@ void External::freeze (int elit) { reset_extended (); int ilit = internalize (elit); unsigned eidx = vidx (elit); - while (eidx >= frozentab.size ()) - frozentab.push_back (0); + if (eidx >= frozentab.size ()) + frozentab.resize (eidx + 1, 0); unsigned & ref = frozentab[eidx]; if (ref < UINT_MAX) { ref++; @@ -366,20 +392,36 @@ void External::check_assumptions_satisfied () { assumptions.size ()); } -void External::check_assumptions_failing () { +void External::check_constraint_satisfied () { + for (const auto lit : constraint) { + if (ival (lit) > 0) { + VERBOSE (1, "checked that constraint is satisfied"); + return; + } + } + FATAL ("constraint not satisfied"); +} + +void External::check_failing () { Solver * checker = new Solver (); checker->prefix ("checker "); #ifdef LOGGING if (internal->opts.log) checker->set ("log", true); #endif - for (const auto & lit : original) + for (const auto lit : original) checker->add (lit); - for (const auto & lit : assumptions) { + for (const auto lit : assumptions) { if (!failed (lit)) continue; LOG ("checking failed literal %d in core", lit); checker->add (lit); checker->add (0); } + if (failed_constraint ()) { + LOG (constraint, "checking failed constraint"); + for (const auto lit : constraint) + checker->add (lit); + } else if (constraint.size ()) + LOG (constraint, "constraint satisfied and ignored"); int res = checker->solve (); if (res != 20) FATAL ("failed assumptions do not form a core"); delete checker; diff --git a/src/external.hpp b/src/external.hpp index a7fb452b..bd44451d 100644 --- a/src/external.hpp +++ b/src/external.hpp @@ -61,6 +61,7 @@ struct External { vector e2i; // External 'idx' to internal 'lit'. vector assumptions; // External assumptions. + vector constraint; // External constraint. Terminated by zero. // The extension stack for reconstructing complete satisfying assignments // (models) of the original external formula is kept in this external @@ -170,7 +171,8 @@ struct External { void mark (vector & map, int elit) { const unsigned ulit = elit2ulit (elit); - while (ulit >= map.size ()) map.push_back (false); + if (ulit >= map.size ()) + map.resize (ulit + 1, false); map[ulit] = true; } @@ -273,6 +275,24 @@ struct External { // Other important non IPASIR functions. + /*----------------------------------------------------------------------*/ + + // Add literal to external constraint. + // + void constrain (int elit); + + // Returns true if 'solve' returned 20 because of the constraint. + // + bool failed_constraint (); + + // Deletes the current constraint clause. Called on + // 'transition_to_unknown_state' and if a new constraint is added. Can be + // called directly using the API. + // + void reset_constraint (); + + /*----------------------------------------------------------------------*/ + int lookahead(); CaDiCaL::CubesWithStatus generate_cubes(int, int); @@ -304,7 +324,8 @@ struct External { // Check solver behaves as expected during testing and debugging. void check_assumptions_satisfied (); - void check_assumptions_failing (); + void check_constraint_satisfied (); + void check_failing (); void check_solution_on_learned_clause (); void check_solution_on_shrunken_clause (Clause *); diff --git a/src/gates.cpp b/src/gates.cpp index ae634630..5b9e0551 100644 --- a/src/gates.cpp +++ b/src/gates.cpp @@ -187,12 +187,14 @@ void Internal::find_and_gate (Eliminator & eliminator, int pivot) { bool all_literals_marked = true; unsigned arity = 0; + int satisfied = 0; + for (const auto & lit : *c) { if (lit == -pivot) continue; assert (lit != pivot); signed char tmp = val (lit); if (tmp < 0) continue; - assert (!tmp); + if (tmp > 0) { satisfied = lit; break; } tmp = marked (lit); if (tmp < 0) { arity++; continue; } all_literals_marked = false; @@ -201,6 +203,12 @@ void Internal::find_and_gate (Eliminator & eliminator, int pivot) { if (!all_literals_marked) continue; + if (satisfied) { + LOG (c, "satisfied by %d candidate base clause", satisfied); + mark_garbage (c); + continue; + } + #ifdef LOGGING if (opts.log) { Logger::print_log_prefix (this); diff --git a/src/heap.hpp b/src/heap.hpp index 5e470afe..84f691dd 100644 --- a/src/heap.hpp +++ b/src/heap.hpp @@ -28,7 +28,8 @@ template class heap { // Map an element to its position entry in the 'pos' map. // unsigned & index (unsigned e) { - while ((size_t) e >= pos.size ()) pos.push_back (invalid_heap_position); + if (e >= pos.size ()) + pos.resize (1 + (size_t) e, invalid_heap_position); unsigned & res = pos[e]; assert (res == invalid_heap_position || (size_t) res < array.size ()); return res; diff --git a/src/internal.cpp b/src/internal.cpp index 2a7cebbc..b0bc21db 100644 --- a/src/internal.cpp +++ b/src/internal.cpp @@ -31,6 +31,8 @@ Internal::Internal () best_assigned (0), target_assigned (0), no_conflict_until (0), + unsat_constraint (false), + marked_failed (true), proof (0), checker (0), tracer (0), @@ -97,14 +99,14 @@ void Internal::enlarge_vals (size_t new_vsize) { template static void enlarge_init (vector & v, size_t N, const T & i) { - while (v.size () < N) - v.push_back (i); + if (v.size () < N) + v.resize (N, i); } template static void enlarge_only (vector & v, size_t N) { - while (v.size () < N) - v.push_back (T ()); + if (v.size () < N) + v.resize (N, T ()); } template @@ -195,6 +197,7 @@ int Internal::cdcl_loop_with_inprocessing () { while (!res) { if (unsat) res = 20; + else if (unsat_constraint) res = 20; else if (!propagate ()) analyze (); // propagate and analyze else if (iterating) iterate (); // report learned unit else if (satisfied ()) res = 10; // found model @@ -554,6 +557,7 @@ int Internal::local_search () { if (unsat) return 0; if (!max_var) return 0; if (!opts.walk) return 0; + if (constraint.size ()) return 0; int res = 0; @@ -601,7 +605,7 @@ int Internal::solve (bool preprocess_only) { int Internal::already_solved () { int res = 0; - if (unsat) { + if (unsat || unsat_constraint) { LOG ("already inconsistent"); res = 20; } else { diff --git a/src/internal.hpp b/src/internal.hpp index 840d4c62..07762356 100644 --- a/src/internal.hpp +++ b/src/internal.hpp @@ -182,6 +182,9 @@ struct Internal { vector trail; // currently assigned literals vector clause; // simplified in parsing & learning vector assumptions; // assumed literals + vector constraint; // literals of the constraint + bool unsat_constraint; // constraint used for unsatisfiability? + bool marked_failed; // are the failed assumptions marked? vector original; // original added literals vector levels; // decision levels in learned clause vector analyzed; // analyzed literals in 'analyze' @@ -915,25 +918,27 @@ struct Internal { bool decompose_round(); void decompose(); + void reset_limits(); // Reset after 'solve' call. + // Assumption handling. // void assume(int); // New assumption literal. + bool failed(int lit); // Literal failed assumption? void reset_assumptions(); // Reset after 'solve' call. - void reset_limits(); // Reset after 'solve' call. void failing(); // Prepare failed assumptions. - bool failed(int lit) { // Literal failed assumption? - Flags &f = flags(lit); - const unsigned bit = bign(lit); - return (f.failed & bit) != 0; - } - - bool assumed(int lit) { // Marked as assumption. + bool assumed(int lit) { // Marked as assumption. Flags &f = flags(lit); const unsigned bit = bign(lit); return (f.assumed & bit) != 0; } + // Add temporary clause as constraint. + // + void constrain(int); // Add literal to constraint. + bool failed_constraint(); // Was constraint used to proof unsatisfiablity? + void reset_constraint(); // Reset after 'solve' call. + // Forcing decision variables to a certain phase. // void phase(int lit); diff --git a/src/lucky.cpp b/src/lucky.cpp index 25f34cd7..43c96f6a 100644 --- a/src/lucky.cpp +++ b/src/lucky.cpp @@ -277,8 +277,8 @@ int Internal::lucky_phases () { // TODO: Some of the lucky assignments can also be found if there are // assumptions, but this is not completely implemented nor tested yet. - // - if (!assumptions.empty ()) return 0; + // Nothing done for constraint either. + if (!assumptions.empty () || !constraint.empty ()) return 0; START (search); START (lucky); diff --git a/src/mobical.cpp b/src/mobical.cpp index 9b373b1b..36442e64 100644 --- a/src/mobical.cpp +++ b/src/mobical.cpp @@ -452,11 +452,13 @@ struct Call { RESET = (1<<24), + CONSTRAIN = (1<<25), + ALWAYS = VARS | ACTIVE | REDUNDANT | IRREDUNDANT | FREEZE | FROZEN | MELT | LIMIT | OPTIMIZE | DUMP | STATS | RESERVE | FIXED, CONFIG = INIT | SET | CONFIGURE | ALWAYS, - BEFORE = ADD | ASSUME | ALWAYS, + BEFORE = ADD | CONSTRAIN | ASSUME | ALWAYS, PROCESS = SOLVE | SIMPLIFY | LOOKAHEAD | CUBING, AFTER = VAL | FAILED | ALWAYS, }; @@ -602,6 +604,14 @@ struct AddCall : public Call { const char * keyword () { return "add"; } }; +struct ConstrainCall : public Call { + ConstrainCall (int l) : Call (CONSTRAIN, l) { } + void execute (Solver * & s) { s->constrain (arg); } + void print (ostream & o) { o << "constrain " << arg << endl; } + Call * copy () { return new ConstrainCall (arg); } + const char * keyword () { return "constrain"; } +}; + struct AssumeCall : public Call { AssumeCall (int l) : Call (ASSUME, l) { } void execute (Solver * & s) { s->assume (arg); } @@ -881,6 +891,7 @@ class Trace { void generate_queries (Random &); void generate_reserve (Random &, int vars); void generate_clause (Random &, int minvars, int maxvars, int uniform); + void generate_constraint (Random &, int minvars, int maxvars, int uniform); void generate_assume (Random &, int vars); void generate_process (Random &); void generate_values (Random &, int vars); @@ -1183,6 +1194,21 @@ void Trace::generate_clause (Random & random, push_back (new AddCall (0)); } +void Trace::generate_constraint (Random & random, + int minvars, int maxvars, + int uniform) { + assert (minvars <= maxvars); + int maxsize = maxvars - minvars + 1; + int size = uniform ? uniform : pick_size (random, maxsize); + vector clause; + for (int i = 0; i < size; i++) { + int lit = pick_literal (random, minvars, maxvars, clause); + push_back (new ConstrainCall (lit)); + clause.push_back (lit); + } + push_back (new ConstrainCall (0)); +} + /*------------------------------------------------------------------------*/ void Trace::generate_assume (Random & random, int vars) { @@ -1376,6 +1402,7 @@ void Trace::generate (uint64_t i, uint64_t s) { generate_reserve (random, maxvars), generate_clause (random, minvars, maxvars, uniform); + generate_constraint (random, minvars, maxvars, uniform); generate_assume (random, maxvars); generate_melt (random); generate_freeze (random, maxvars); @@ -1996,6 +2023,7 @@ bool Trace::reduce_values (int expected) { static bool has_lit_arg_type (Call * c) { switch (c->type) { case Call::ADD: + case Call::CONSTRAIN: case Call::ASSUME: case Call::FREEZE: case Call::MELT: @@ -2023,8 +2051,8 @@ void Trace::map_variables (int expected) { if (!c->arg) continue; if (c->arg == INT_MIN) continue; int idx = abs (c->arg); - while (variables.size () <= (size_t) idx) - variables.push_back (0); + if (variables.size () <= (size_t) idx) + variables.resize (1 + (size_t) idx, 0); variables[idx]++; } int gaps = 0, max_idx = 0; @@ -2164,7 +2192,7 @@ static bool is_valid_char (int ch) { } void Reader::parse () { - int ch, lit = 0, val = 0, state = 0, adding = 0, solved = 0; + int ch, lit = 0, val = 0, state = 0, adding = 0, constraining = 0, solved = 0; const bool enforce = !mobical.donot.enforce; Call * before_trigger = 0; char line[80]; @@ -2284,6 +2312,15 @@ void Reader::parse () { error ("invalid literal '%d' as argument to 'add'", lit); adding = lit; c = new AddCall (lit); + } else if (!strcmp (keyword, "constrain")) { + if (!first) error ("argument to 'constrain' missing"); + if (!parse_int_str (first, lit)) + error ("invalid argument '%s' to 'constrain'", first); + if (second) error ("additional argument '%s' to 'constrain'", second); + if (enforce && lit == INT_MIN) + error ("invalid literal '%d' as argument to 'constrain'", lit); + constraining = lit; + c = new ConstrainCall (lit); } else if (!strcmp (keyword, "assume")) { if (!first) error ("argument to 'assume' missing"); if (!parse_int_str (first, lit)) @@ -2428,6 +2465,9 @@ void Reader::parse () { if (adding && c->type != Call::ADD && c->type != Call::RESET) error("'%s' after 'add %d' without 'add 0'", c->keyword(), adding); + if (constraining && c->type != Call::CONSTRAIN && c->type != Call::RESET) + error("'%s' after 'constrain %d' without 'constrain 0'", c->keyword(), constraining); + int new_state = state; switch (c->type) { diff --git a/src/occs.cpp b/src/occs.cpp index d7965899..89952aa3 100644 --- a/src/occs.cpp +++ b/src/occs.cpp @@ -7,8 +7,8 @@ namespace CaDiCaL { // Occurrence lists. void Internal::init_occs () { - while (otab.size () < 2*vsize) - otab.push_back (Occs ()); + if (otab.size () < 2*vsize) + otab.resize (2*vsize, Occs ()); LOG ("initialized occurrence lists"); } @@ -24,8 +24,8 @@ void Internal::reset_occs () { void Internal::init_noccs () { assert (ntab.empty ()); - while (ntab.size () < 2*vsize) - ntab.push_back (0); + if (ntab.size () < 2*vsize) + ntab.resize (2*vsize, 0); LOG ("initialized two-sided occurrence counters"); } diff --git a/src/options.hpp b/src/options.hpp index a1b29343..e7c64bc9 100644 --- a/src/options.hpp +++ b/src/options.hpp @@ -33,6 +33,7 @@ OPTION( bumpreason, 1, 0, 1,0,0,1, "bump reason literals too") \ OPTION( bumpreasondepth, 1, 1, 3,0,0,1, "bump reason depth") \ OPTION( check, 0, 0, 1,0,0,0, "enable internal checking") \ OPTION( checkassumptions, 1, 0, 1,0,0,0, "check assumptions satisfied") \ +OPTION( checkconstraint, 1, 0, 1,0,0,0, "check constraint satisfied") \ OPTION( checkfailed, 1, 0, 1,0,0,0, "check failed literals form core") \ OPTION( checkfrozen, 0, 0, 1,0,0,0, "check all frozen semantics") \ OPTION( checkproof, 1, 0, 1,0,0,0, "check proof internally") \ diff --git a/src/restart.cpp b/src/restart.cpp index 20df6d23..dd50eeb5 100644 --- a/src/restart.cpp +++ b/src/restart.cpp @@ -69,10 +69,14 @@ bool Internal::restarting () { // decision exists top (in which case we do not reuse any level). int Internal::reuse_trail () { - if (!opts.restartreusetrail) return assumptions.size (); + const int trivial_decisions = assumptions.size () + // Plus 1 if the constraint is satisfied via implications of assumptions + // and a pseudo-decision level was introduced + + !control[assumptions.size () + 1].decision; + if (!opts.restartreusetrail) return trivial_decisions; int decision = next_decision_variable (); assert (1 <= decision); - int res = assumptions.size (); + int res = trivial_decisions; if (use_scores ()) { while (res < level && score_smaller (this)(decision, abs (control[res+1].decision))) @@ -82,7 +86,7 @@ int Internal::reuse_trail () { while (res < level && bumped (control[res+1].decision) > limit) res++; } - int reused = res - assumptions.size (); + int reused = res - trivial_decisions; if (reused > 0) { stats.reused++; stats.reusedlevels += reused; diff --git a/src/restore.cpp b/src/restore.cpp index 39f07a7b..ce6974a8 100644 --- a/src/restore.cpp +++ b/src/restore.cpp @@ -77,7 +77,7 @@ void External::restore_clauses () { "forced to restore all clauses"); unsigned numtainted = 0; - for (const auto & b : tainted) + for (const auto b : tainted) if (b) numtainted++; PHASE ("restore", internal->stats.restorations, diff --git a/src/solver.cpp b/src/solver.cpp index 13c8d72d..31b16105 100644 --- a/src/solver.cpp +++ b/src/solver.cpp @@ -48,10 +48,12 @@ void Solver::transition_to_unknown_state () { LOG ("API leaves state %sSATISFIED%s", tout.emph_code (), tout.normal_code ()); external->reset_assumptions (); + external->reset_constraint (); } else if (state () == UNSATISFIED) { LOG ("API leaves state %sUNSATISFIED%s", tout.emph_code (), tout.normal_code ()); external->reset_assumptions (); + external->reset_constraint (); } if (state () != UNKNOWN) STATE (UNKNOWN); } @@ -330,6 +332,8 @@ Solver::Solver () { } #endif + adding_clause = false; + adding_constraint = false; _state = INITIALIZING; internal = new Internal (); TRACE ("init"); @@ -526,11 +530,24 @@ void Solver::add (int lit) { if (lit) REQUIRE_VALID_LIT (lit); transition_to_unknown_state (); external->add (lit); - if (lit) STATE (ADDING); - else STATE (UNKNOWN); + adding_clause = lit; + if (adding_clause) STATE (ADDING); + else if (!adding_constraint) STATE (UNKNOWN); LOG_API_CALL_END ("add", lit); } +void Solver::constrain (int lit) { + TRACE ("constrain", lit); + REQUIRE_VALID_STATE (); + if (lit) REQUIRE_VALID_LIT (lit); + transition_to_unknown_state (); + external->constrain (lit); + adding_constraint = lit; + if (adding_constraint) STATE (ADDING); + else if (!adding_clause) STATE (UNKNOWN); + LOG_API_CALL_END ("constrain", lit); +} + void Solver::assume (int lit) { TRACE ("assume", lit); REQUIRE_VALID_STATE (); @@ -568,6 +585,14 @@ void Solver::reset_assumptions () { LOG_API_CALL_END ("reset_assumptions"); } +void Solver::reset_constraint () { + TRACE ("reset_constraint"); + REQUIRE_VALID_STATE (); + transition_to_unknown_state (); + external->reset_constraint (); + LOG_API_CALL_END ("reset_constraint"); +} + /*------------------------------------------------------------------------*/ int Solver::call_external_solve_and_check_results (bool preprocess_only) { @@ -628,6 +653,7 @@ int Solver::val (int lit) { REQUIRE_VALID_LIT (lit); REQUIRE (state () == SATISFIED, "can only get value in satisfied state"); + if (!external->extended) external->extend (); int res = external->ival (lit); LOG_API_CALL_RETURNS ("val", lit, res); return res; @@ -644,6 +670,16 @@ bool Solver::failed (int lit) { return res; } +bool Solver::constraint_failed () { + TRACE ("constraint_failed"); + REQUIRE_VALID_STATE (); + REQUIRE (state () == UNSATISFIED, + "can only determine if constraint failed in unsatisfied state"); + bool res = external->failed_constraint (); + LOG_API_CALL_RETURNS ("constraint_failed", res); + return res; +} + int Solver::fixed (int lit) const { TRACE ("fixed", lit); REQUIRE_VALID_STATE (); diff --git a/src/walk.cpp b/src/walk.cpp index bbda8371..6c1018f6 100644 --- a/src/walk.cpp +++ b/src/walk.cpp @@ -334,7 +334,7 @@ void Internal::walk_flip_lit (Walker & walker, int lit) { LOG ("trying to brake %zd watched clauses", ws.size ()); - for (const auto w : ws) { + for (const auto & w : ws) { Clause * d = w.clause; LOG (d, "unwatch %d in", -lit); int * literals = d->literals, replacement = 0, prev = -lit; diff --git a/src/watch.cpp b/src/watch.cpp index 158b9da3..c1c4a156 100644 --- a/src/watch.cpp +++ b/src/watch.cpp @@ -4,8 +4,8 @@ namespace CaDiCaL { void Internal::init_watches () { assert (wtab.empty ()); - while (wtab.size () < 2*vsize) - wtab.push_back (Watches ()); + if (wtab.size () < 2*vsize) + wtab.resize (2*vsize, Watches ()); LOG ("initialized watcher tables"); } @@ -88,10 +88,8 @@ void Internal::sort_watches () { if (w.binary ()) *j++ = w; else saved.push_back (w); } - ws.resize (j - ws.begin ()); - for (const auto & w : saved) - ws.push_back (w); + std::copy (saved.cbegin (), saved.cend (), j); saved.clear (); } diff --git a/test/api/example_constraint.cpp b/test/api/example_constraint.cpp new file mode 100644 index 00000000..34ab79df --- /dev/null +++ b/test/api/example_constraint.cpp @@ -0,0 +1,77 @@ +#include "../../src/cadical.hpp" +#ifdef NDEBUG +#undef NDEBUG +#endif +#include + +// This is the example from the header file + +int main () { + + CaDiCaL::Solver * solver = new CaDiCaL::Solver; + + // ------------------------------------------------------------------ + // Encode Problem and check without assumptions. + + enum { TIE = 1, SHIRT = 2 }; + + solver->add (-TIE), solver->add (SHIRT), solver->add (0); + solver->add (TIE), solver->add (SHIRT), solver->add (0); + solver->add (-TIE), solver->add (-SHIRT), solver->add (0); + + int res = solver->solve (); // Solve instance. + assert (res == 10); // Check it is 'SATISFIABLE'. + + res = solver->val (TIE); // Obtain assignment of 'TIE'. + assert (res < 0); // Check 'TIE' assigned to 'false'. + + res = solver->val (SHIRT); // Obtain assignment of 'SHIRT'. + assert (res > 0); // Check 'SHIRT' assigned to 'true'. + + // ------------------------------------------------------------------ + // Incrementally solve again under one assumption. + + solver->assume (TIE); // Now force 'TIE' to true. + + res = solver->solve (); // Solve again incrementally. + assert (res == 20); // Check it is 'UNSATISFIABLE'. + + res = solver->failed (TIE); // Check 'TIE' responsible. + assert (res); // Yes, 'TIE' in core. + + res = solver->failed (SHIRT); // Check 'SHIRT' responsible. + assert (!res); // No, 'SHIRT' not in core. + + // ------------------------------------------------------------------ + // Incrementally solve with constraint. + + solver->constrain (TIE), solver->constrain (-SHIRT), solver->constrain (0); + + res = solver->solve (); // Solve again incrementally. + assert (res == 20); // Check it is 'UNSATISFIABLE'. + + res = + solver->failed_constraint (); // Check constraint responsible. + assert (res); // Yes, constraint was used. + + // ------------------------------------------------------------------ + // Incrementally solve once more under another assumption. + + solver->assume (-SHIRT); // Now force 'SHIRT' to false. + + res = solver->solve (); // Solve again incrementally. + assert (res == 20); // Check it is 'UNSATISFIABLE'. + + res = solver->failed (TIE); // Check 'TIE' responsible. + assert (!res); // No, 'TIE' not in core. + + res = solver->failed (-SHIRT); // Check '!SHIRT' responsible. + assert (res); // Yes, '!SHIRT' in core. + + // ------------------------------------------------------------------ + + + delete solver; + + return 0; +} diff --git a/test/trace/reg0057.trace b/test/trace/reg0057.trace new file mode 100644 index 00000000..dcea1875 --- /dev/null +++ b/test/trace/reg0057.trace @@ -0,0 +1,54 @@ +0 init +1 set elimboundmin -1 +2 set elimequivs 0 +3 set elimint 1 +4 set elimprod 0 +5 set elimsum 0 +6 set vivifymineff 0 +7 add -2 +8 add -7 +9 add 0 +10 add -8 +11 add -11 +12 add 0 +13 add -4 +14 add -5 +15 add 0 +16 add 8 +17 add 1 +18 add 4 +19 add 0 +20 add 3 +21 add 6 +22 add 0 +23 add -3 +24 add -9 +25 add 0 +26 add 1 +27 add 3 +28 add 9 +29 add 0 +30 add 8 +31 add -10 +32 add 0 +33 add 5 +34 add -4 +35 add 0 +36 add 2 +37 add -3 +38 add 1 +39 add 0 +40 add 4 +41 add 3 +42 add -9 +43 add 0 +44 add -3 +45 add 6 +46 add 0 +47 add 7 +48 add 9 +49 add 0 +50 assume -6 +51 solve 0 +52 assume -1 +53 solve 0 diff --git a/test/trace/reg0058.trace b/test/trace/reg0058.trace new file mode 100644 index 00000000..24536ea1 --- /dev/null +++ b/test/trace/reg0058.trace @@ -0,0 +1,54 @@ +0 init +1 set elimequivs 0 +2 set elimint 1 +3 set elimprod 0 +4 set elimsum 0 +5 set vivifymineff 0 +6 set elimboundmin -1 +7 set lucky 0 +8 add -2 +9 add -7 +10 add 0 +11 add -8 +12 add 1 +13 add 0 +14 add -4 +15 add -5 +16 add 0 +17 add 8 +18 add 1 +19 add 4 +20 add 0 +21 add 3 +22 add 6 +23 add 0 +24 add -3 +25 add -9 +26 add 0 +27 add 1 +28 add 3 +29 add 9 +30 add 0 +31 add 8 +32 add 1 +33 add 0 +34 add 5 +35 add -4 +36 add 0 +37 add 2 +38 add -3 +39 add 1 +40 add 0 +41 add 4 +42 add 3 +43 add -9 +44 add 0 +45 add -3 +46 add 6 +47 add 0 +48 add 7 +49 add 9 +50 add 0 +51 assume -6 +52 solve 0 +53 solve 0