diff options
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/minisat/core/Solver.h | 6 | ||||
-rw-r--r-- | src/prop/minisat/minisat.cpp | 10 | ||||
-rw-r--r-- | src/prop/minisat/minisat.h | 4 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 14 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 16 | ||||
-rw-r--r-- | src/prop/sat_solver.h | 10 |
6 files changed, 57 insertions, 3 deletions
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index a9ee25c11..f4aa04e4d 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -531,12 +531,12 @@ protected: 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; diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index b09ffd685..293e7175b 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -259,6 +259,16 @@ bool MinisatSatSolver::isDecision(SatVariable decn) 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(); diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index a4bd1e7a0..0e6ca28b8 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -85,6 +85,10 @@ class MinisatSatSolver : public CDCLTSatSolverInterface 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; } diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 70401c56d..63591e74b 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -340,6 +340,20 @@ bool PropEngine::isDecision(Node lit) const { 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(); diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 631317c2d..a12816906 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -157,6 +157,22 @@ class PropEngine 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. * */ diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index 1c64c92c2..963810594 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -168,6 +168,16 @@ class CDCLTSatSolverInterface : public SatSolver 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 */ |