22 #ifndef _cvc3__include__search_impl_base_h_
23 #define _cvc3__include__search_impl_base_h_
32 class SearchEngineRules;
33 class VariableManager;
267 virtual void getCounterExample(std::vector<Expr>& assertions,
bool inOrder =
true);
API to to a generic proof search engine.
Data structure of expressions in CVC3.
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Representation of a DP-suggested splitter.
Abstract API to the proof search engine.
TheoryCore::CoreSatAPI * d_coreSatAPI_implBase
CDO< int > d_bottomScope
The bottom-most scope for the current call to checkSAT (where conflict clauses are still valid)...
CDMap< Expr, bool > d_applyCNFRulesCache
Cache for applyCNFRules()
void getUserAssumptions(std::vector< Expr > &assumptions)
Get all assumptions made in this and all previous contexts.
Literal newLiteral(const Expr &e)
Construct a Literal out of an Expr or return an existing one.
Theorem d_lastValid
Theorem from the last successful checkValid call. It is used by getProof and getAssumptions.
virtual bool isAssumption(const Expr &e)
Check if the formula has been assumed.
virtual QueryResult checkValidInternal(const Expr &e)=0
Checks the validity of a formula in the current context.
virtual Proof getProof()
Returns the proof term for the last proven query.
virtual Theorem getImpliedLiteral()
Return next literal implied by last assertion. Null Expr if none.
Theorem findInCNFCache(const Expr &e)
Find a theorem phi <=> v by phi, where v is a literal.
VariableManager * d_vm
Variable manager for classes Variable and Literal.
CDMap< Expr, bool > d_enqueueCNFCache
Cache for enqueueCNF()
Theorem replaceITE(const Expr &e)
Replaces ITE subexpressions in e with variables.
CDMap< Expr, Theorem > d_cnfCache
Backtracking cache for the CNF generator.
bool isPropClause(const Expr &e)
Check if e is a propositional clause.
Theorem iffMP(const Theorem &e1, const Theorem &e1_iff_e2)
e1 AND (e1 IFF e2) ==> e2
virtual void addNonLiteralFact(const Theorem &thm)=0
Notify the search engine about a new non-literal fact.
void applyCNFRules(const Theorem &e)
FIXME: write a comment.
void getInternalAssumptions(std::vector< Expr > &assumptions)
Get assumptions made internally in this and all previous contexts.
virtual QueryResult restartInternal(const Expr &e)=0
Reruns last check with e as an additional assumption.
void returnFromCheck()
Returns to context immediately before last call to checkValid.
Theorem simplify(const Expr &e)
Top-level simplifier.
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
CDMap< Expr, Theorem > d_assumptions
Maintain the list of current assumptions (user asserts and splitters) for getAssumptions().
virtual void pop()
Restore last checkpoint.
virtual Theorem lastThm()
Returns the result of the most recent valid theorem.
virtual Theorem newIntAssumption(const Expr &e)
Add a new internal asserion.
bool isCNFVar(const Expr &e)
Check whether e is a fresh variable introduced by the CNF converter.
bool isGoodSplitter(const Expr &e)
Check if a splitter is required for completeness.
ExprHashMap< bool > d_lastCounterExample
Assumptions from the last unsuccessful checkValid call. These are used by getCounterExample.
virtual void addLiteralFact(const Theorem &thm)=0
Notify the search engine about a new literal fact.
Theorem getImpliedLiteral(void)
Return the next implied literal (NULL Theorem if none)
Theorem newUserAssumption(const Expr &e)
Generate and add a new assertion to the set of assertions in the current context. This should only be...
virtual void getAssumptions(std::vector< Expr > &assumptions)
Get all assumptions made in this and all previous contexts.
const bool * d_ifLiftOption
Flag: whether to convert term ITEs into CNF.
void addToCNFCache(const Theorem &thm)
Cache a theorem phi <=> v by phi, where v is a literal.
const Expr & falseExpr()
Return FALSE Expr.
Interface class for callbacks to SAT from Core.
void enqueueCNFrec(const Theorem &theta)
Recursive version of enqueueCNF()
void processResult(const Theorem &res, const Expr &e)
Process result of checkValid.
int scopeLevel()
Return the current scope level (for convenience)
Splitter & operator=(const Splitter &s)
Assignment.
virtual void registerAtom(const Expr &e)
Register an atomic formula of interest.
virtual QueryResult restart(const Expr &e, Theorem &result)
Reruns last check with e as an additional assumption.
void addCNFFact(const Theorem &thm, bool fromCore=false)
Add a new fact to the search engine bypassing CNF converter.
ContextManager * getCM() const
void enqueueCNF(const Theorem &theta)
Translate theta to CNF and enqueue the new clauses.
virtual ~SearchImplBase()
Destructor.
size_t count(const Key &k) const
API to to a generic proof search engine (a.k.a. SAT solver)
CDMap< Expr, bool > d_cnfVars
Backtracking set of new variables generated by CNF translator.
virtual FormulaValue getValue(const CVC3::Expr &e)
virtual void registerAtom(const Expr &e, const Theorem &thm)
void addFact(const Theorem &thm)
Add a new fact to the search engine from the core.
CDList< Splitter > d_dpSplitters
Backtracking ordered set of DP-suggested splitters.
const bool * d_origFormulaOption
Flag: Preserve the original formula with +cnf (for splitter heuristics)
CDMap< Expr, Theorem > d_replaceITECache
Cache for replaceITE()
const bool * d_cnfOption
Command line flag whether to convert to CNF.
bool isClause(const Expr &e)
Check if e is a clause (a literal, or a disjunction of literals)
virtual void getCounterExample(std::vector< Expr > &assertions, bool inOrder=true)
Will return the set of assertions which make the queried formula false.
Theorem simplify(const Theorem &e)
Our version of simplifier: take Theorem(e), apply simplifier to get Theorem(e==e'), return Theorem(e')
const bool * d_ignoreCnfVarsOption
Flag: ignore auxiliary CNF variables when searching for a splitter.
Theory * theoryOf(int kind)
Return the theory associated with a kind.
virtual void addSplitter(const Expr &e, int priority)
Suggest a splitter to the SearchEngine.
virtual const Assumptions & getAssumptionsUsed()
Returns the set of assumptions used in the proof. It should be a subset of getAssumptions().
SearchImplBase(TheoryCore *core)
Constructor.
Splitter(const Literal &lit)
Constructor.
TheoryCore * d_core
Access to theory reasoning.
virtual QueryResult checkValid(const Expr &e, Theorem &result)
Similar to checkValidInternal(), only returns Theorem(e) or Null.
virtual void push()
Push a checkpoint.