diff options
Diffstat (limited to 'src/prop/sat.h')
-rw-r--r-- | src/prop/sat.h | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/src/prop/sat.h b/src/prop/sat.h index be3ed244b..e86443827 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -137,6 +137,12 @@ class SatSolver : public SatInputInterface { /** Context we will be using to synchronzie the sat solver */ context::Context* d_context; + /** + * Set of all lemmas that have been "shared" in the portfolio---i.e., + * all imported and exported lemmas. + */ + std::hash_set<Node, NodeHashFunction> d_shared; + /* Pointer to the concrete SAT solver. Including this via the preprocessor saves us a level of indirection vs, e.g., defining a sub-class for each solver. */ @@ -263,6 +269,8 @@ public: void notifyRestart(); + void notifyNewLemma(SatClause& lemma); + SatLiteral getNextReplayDecision(); void logDecision(SatLiteral lit); @@ -294,6 +302,12 @@ inline SatSolver::SatSolver(PropEngine* propEngine, d_minisat->random_var_freq = Options::current()->satRandomFreq; d_minisat->random_seed = Options::current()->satRandomSeed; + // Give access to all possible options in the sat solver + d_minisat->var_decay = Options::current()->satVarDecay; + d_minisat->clause_decay = Options::current()->satClauseDecay; + d_minisat->restart_first = Options::current()->satRestartFirst; + d_minisat->restart_inc = Options::current()->satRestartInc; + d_statistics.init(d_minisat); } |