diff options
Diffstat (limited to 'src/theory/smt_engine_subsolver.h')
| -rw-r--r-- | src/theory/smt_engine_subsolver.h | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/src/theory/smt_engine_subsolver.h b/src/theory/smt_engine_subsolver.h index 0e1af29db..5de65a5d2 100644 --- a/src/theory/smt_engine_subsolver.h +++ b/src/theory/smt_engine_subsolver.h @@ -113,6 +113,31 @@ Result checkWithSubsolver(Node query, bool needsTimeout = false, unsigned long timeout = 0); +//--------------- utilities + +/** + * Assuming smt has just been called to check-sat and returned "SAT", this + * method adds the model for d_vars to mvs. + */ +void getModelFromSubsolver(SolverEngine& smt, + const std::vector<Node>& vars, + std::vector<Node>& mvs); + +/** + * Assuming smt has just been called to check-sat and returned "UNSAT", this + * method get the unsat core and adds it to uasserts. + * + * The assertions in the argument queryAsserts (which we are not interested + * in tracking in the unsat core) are excluded from uasserts. + * If one of the formulas in queryAsserts was in the unsat core, then this + * method returns true. Otherwise, this method returns false. + */ +bool getUnsatCoreFromSubsolver(SolverEngine& smt, + const std::unordered_set<Node>& queryAsserts, + std::vector<Node>& uasserts); +/** Same as above, without query asserts */ +void getUnsatCoreFromSubsolver(SolverEngine& smt, std::vector<Node>& uasserts); + } // namespace theory } // namespace cvc5 |