The bitblast solver currently uses solving under assumptions for all facts that are sent to the bit-vector solver. For input facts on user-level 0 we can however assert the fact to the SAT solver, which allows the SAT solver to do more preprocessing. This PR adds the option to assert user-level 0 input facts, which is disabled by default.
name = "simple"
help = "Enables simple bitblasting solver with proof support."
+[[option]]
+ name = "bvAssertInput"
+ category = "regular"
+ long = "bv-assert-input"
+ type = "bool"
+ default = "false"
+ help = "assert input assertions on user-level 0 instead of assuming them in the bit-vector SAT solver"
+
bool isPropagated (Var x) const; // Does the variable have a propagated variables
bool isPropagatedBy (Var x, const Clause& c) const; // Is the value of the variable propagated by the clause Clause C
- int level (Var x) const;
- int user_level (Var x) const; // User level at which this variable was asserted
- int intro_level (Var x) const; // User level at which this variable was created
int trail_index (Var x) const; // Index in the trail
double progressEstimate () const; // DELETE THIS ?? IT'S NOT VERY USEFUL ...
public:
+ int level (Var x) const;
+ int user_level (Var x) const; // User level at which this variable was asserted
+ int intro_level (Var x) const; // User level at which this variable was created
bool withinBudget (uint64_t amount) const;
bool withinBudget(Resource r) const;
return d_minisat->isDecision( decn );
}
+int32_t MinisatSatSolver::getDecisionLevel(SatVariable v) const
+{
+ return d_minisat->level(v);
+}
+
+int32_t MinisatSatSolver::getIntroLevel(SatVariable v) const
+{
+ return d_minisat->intro_level(v);
+}
+
SatProofManager* MinisatSatSolver::getProofManager()
{
return d_minisat->getProofManager();
bool isDecision(SatVariable decn) const override;
+ int32_t getDecisionLevel(SatVariable v) const override;
+
+ int32_t getIntroLevel(SatVariable v) const override;
+
/** Retrieve a pointer to the unerlying solver. */
Minisat::SimpSolver* getSolver() { return d_minisat; }
return d_satSolver->isDecision(d_cnfStream->getLiteral(lit).getSatVariable());
}
+int32_t PropEngine::getDecisionLevel(Node lit) const
+{
+ Assert(isSatLiteral(lit));
+ return d_satSolver->getDecisionLevel(
+ d_cnfStream->getLiteral(lit).getSatVariable());
+}
+
+int32_t PropEngine::getIntroLevel(Node lit) const
+{
+ Assert(isSatLiteral(lit));
+ return d_satSolver->getIntroLevel(
+ d_cnfStream->getLiteral(lit).getSatVariable());
+}
+
void PropEngine::printSatisfyingAssignment(){
const CnfStream::NodeToLiteralMap& transCache =
d_cnfStream->getTranslationCache();
*/
bool isDecision(Node lit) const;
+ /**
+ * Return the current decision level of `lit`.
+ *
+ * @param lit: The node in question, must have an associated SAT literal.
+ * @return Decision level of the SAT variable of `lit` (phase is disregarded),
+ * or -1 if `lit` has not been assigned yet.
+ */
+ int32_t getDecisionLevel(Node lit) const;
+
+ /**
+ * Return the user-context level when `lit` was introduced..
+ *
+ * @return User-context level or -1 if not yet introduced.
+ */
+ int32_t getIntroLevel(Node lit) const;
+
/**
* Checks the current context for satisfiability.
*
virtual bool isDecision(SatVariable decn) const = 0;
+ /**
+ * Return the current decision level of `lit`.
+ */
+ virtual int32_t getDecisionLevel(SatVariable v) const { return -1; }
+
+ /**
+ * Return the user-context level when `lit` was introduced..
+ */
+ virtual int32_t getIntroLevel(SatVariable v) const { return -1; }
+
virtual std::shared_ptr<ProofNode> getProof() = 0;
}; /* class CDCLTSatSolverInterface */
d_nullRegistrar(new prop::NullRegistrar()),
d_nullContext(new context::Context()),
d_bbFacts(s->getSatContext()),
+ d_bbInputFacts(s->getSatContext()),
d_assumptions(s->getSatContext()),
+ d_assertions(s->getSatContext()),
d_invalidateModelCache(s->getSatContext(), true),
d_inSatMode(s->getSatContext(), false),
d_epg(pnm ? new EagerProofGenerator(pnm, s->getUserContext(), "")
}
}
+ NodeManager* nm = NodeManager::currentNM();
+
+ /* Process input assertions bit-blast queue. */
+ while (!d_bbInputFacts.empty())
+ {
+ Node fact = d_bbInputFacts.front();
+ d_bbInputFacts.pop();
+ /* Bit-blast fact and cache literal. */
+ if (d_factLiteralCache.find(fact) == d_factLiteralCache.end())
+ {
+ d_bitblaster->bbAtom(fact);
+ Node bb_fact = d_bitblaster->getStoredBBAtom(fact);
+ d_cnfStream->convertAndAssert(bb_fact, false, false);
+ }
+ d_assertions.push_back(fact);
+ }
+
/* Process bit-blast queue and store SAT literals. */
while (!d_bbFacts.empty())
{
d_bitblaster->bbAtom(fact);
Node bb_fact = d_bitblaster->getStoredBBAtom(fact);
d_cnfStream->ensureLiteral(bb_fact);
-
prop::SatLiteral lit = d_cnfStream->getLiteral(bb_fact);
d_factLiteralCache[fact] = lit;
d_literalFactCache[lit] = fact;
{
std::vector<prop::SatLiteral> unsat_assumptions;
d_satSolver->getUnsatAssumptions(unsat_assumptions);
- Assert(unsat_assumptions.size() > 0);
- std::vector<Node> conflict;
- for (const prop::SatLiteral& lit : unsat_assumptions)
+ Node conflict;
+ // Unsat assumptions produce conflict.
+ if (unsat_assumptions.size() > 0)
{
- conflict.push_back(d_literalFactCache[lit]);
- Debug("bv-bitblast") << "unsat assumption (" << lit
- << "): " << conflict.back() << std::endl;
+ std::vector<Node> conf;
+ for (const prop::SatLiteral& lit : unsat_assumptions)
+ {
+ conf.push_back(d_literalFactCache[lit]);
+ Debug("bv-bitblast")
+ << "unsat assumption (" << lit << "): " << conf.back() << std::endl;
+ }
+ conflict = nm->mkAnd(conf);
}
-
- NodeManager* nm = NodeManager::currentNM();
- d_im.conflict(nm->mkAnd(conflict), InferenceId::BV_BITBLAST_CONFLICT);
+ else // Input assertions produce conflict.
+ {
+ std::vector<Node> assertions(d_assertions.begin(), d_assertions.end());
+ conflict = nm->mkAnd(assertions);
+ }
+ d_im.conflict(conflict, InferenceId::BV_BITBLAST_CONFLICT);
}
}
bool BVSolverBitblast::preNotifyFact(
TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
{
- d_bbFacts.push_back(fact);
+ Valuation& val = d_state.getValuation();
+
+ /**
+ * Check whether `fact` is an input assertion on user-level 0.
+ *
+ * If this is the case we can assert `fact` to the SAT solver instead of
+ * using assumptions.
+ */
+ if (options::bvAssertInput() && val.isSatLiteral(fact)
+ && !val.isDecision(fact) && val.getDecisionLevel(fact) == 0
+ && val.getIntroLevel(fact) == 0)
+ {
+ d_bbInputFacts.push_back(fact);
+ }
+ else
+ {
+ d_bbFacts.push_back(fact);
+ }
+
return false; // Return false to enable equality engine reasoning in Theory.
}
namespace theory {
namespace bv {
+class BBRegistrar;
+
/**
* Bit-blasting solver with support for different SAT back ends.
*/
/** Used for initializing `d_cnfStream`. */
std::unique_ptr<prop::NullRegistrar> d_nullRegistrar;
+
std::unique_ptr<context::Context> d_nullContext;
/** SAT solver back end (configured via options::bvSatSolver. */
*/
context::CDQueue<Node> d_bbFacts;
+ /**
+ * Bit-blast queue for user-level 0 input facts sent to this solver.
+ *
+ * Get populated on preNotifyFact().
+ */
+ context::CDQueue<Node> d_bbInputFacts;
+
/** Corresponds to the SAT literals of the currently asserted facts. */
context::CDList<prop::SatLiteral> d_assumptions;
+ /** Stores the current input assertions. */
+ context::CDList<Node> d_assertions;
+
/** Flag indicating whether `d_modelCache` should be invalidated. */
context::CDO<bool> d_invalidateModelCache;
return d_engine->getPropEngine()->isDecision(lit);
}
+int32_t Valuation::getDecisionLevel(Node lit) const
+{
+ Assert(d_engine != nullptr);
+ return d_engine->getPropEngine()->getDecisionLevel(lit);
+}
+
+int32_t Valuation::getIntroLevel(Node lit) const
+{
+ Assert(d_engine != nullptr);
+ return d_engine->getPropEngine()->getIntroLevel(lit);
+}
+
unsigned Valuation::getAssertionLevel() const{
Assert(d_engine != nullptr);
return d_engine->getPropEngine()->getAssertionLevel();
*/
bool isDecision(Node lit) const;
+ /**
+ * Return the current decision level of `lit`.
+ *
+ * @param lit: The node in question, must have an associated SAT literal.
+ * @return Decision level of the SAT variable of `lit` (phase is disregarded),
+ * or -1 if `lit` has not been assigned yet.
+ */
+ int32_t getDecisionLevel(Node lit) const;
+
+ /**
+ * Return the user-context level when `lit` was introduced..
+ *
+ * @return User-context level or -1 if not yet introduced.
+ */
+ int32_t getIntroLevel(Node lit) const;
+
/**
* Get the assertion level of the SAT solver.
*/
projects / cvc5.git / commitdiff