46 { d_se->addFact(thm); }
48 {
return d_se->newIntAssumption(assump); }
50 { d_se->addSplitter(e, priority); }
51 virtual bool check(
const Expr& e);
54 bool CoreSatAPI_implBase::check(
const Expr& e)
57 int scope = d_se->theoryCore()->getCM()->scopeLevel();
58 d_se->theoryCore()->getCM()->push();
60 d_se->theoryCore()->getCM()->popto(scope);
75 SearchImplBase::Splitter::Splitter(
const Literal& lit): d_lit(lit) {
84 TRACE(
"Splitter",
"Splitter[copy](",
d_lit,
")");
90 if(
this == &s)
return *
this;
94 TRACE(
"Splitter",
"Splitter[assign](", d_lit,
")");
101 TRACE(
"Splitter",
"~Splitter(", d_lit,
")");
113 d_cnfCache(core->getCM()->getCurrentContext()),
114 d_cnfVars(core->getCM()->getCurrentContext()),
124 core->
getFlags()[
"mm"].getString());
144 IF_DEBUG(
if(debugger.trace(
"search verbose")) {
145 ostream& os(debugger.getOS());
146 os <<
"d_assumptions = [";
149 debugger.getOS() <<
"(" << (*i).first <<
" => " << (*i).second <<
"), ";
154 TRACE(
"search verbose",
"newUserAssumption(", e,
155 "): assumption already exists");
160 TRACE(
"search verbose",
"newUserAssumption(", thm,
161 "): created new assumption");
184 TRACE(
"search verbose",
"newIntAssumption(", thm,
185 "): new assumption");
193 if ((*i).first.isUserAssumption()) assumptions.push_back((*i).first);
201 if ((*i).first.isIntAssumption()) assumptions.push_back((*i).first);
209 assumptions.push_back((*i).first);
219 TRACE(
"addCNFFact",
"addCNFFact(", thm.
getExpr(),
") {");
227 TRACE_MSG(
"addCNFFact",
"addCNFFact => }");
232 TRACE(
"search addFact",
"SearchImplBase::addFact(", thm.
getExpr(),
") {");
237 TRACE_MSG(
"search addFact",
"SearchImplBase::addFact => }");
251 (
"Method getCounterExample() (or command COUNTEREXAMPLE) cannot be used\n"
252 " without assumptions activated");
255 (
"Method getCounterExample() (or command COUNTEREXAMPLE)\n"
256 " must be called only after failed QUERY");
286 (
"DUMP_PROOF cannot be used without proofs activated");
289 (
"DUMP_PROOF must be called only after successful QUERY");
301 (
"DUMP_ASSUMPTIONS cannot be used without assumptions activated");
304 (
"DUMP_ASSUMPTIONS must be called only after successful QUERY");
321 "processResult: bad input"
361 TRACE(
"mycnf",
"enqueueCNF(", beta,
") {");
374 TRACE(
"mycnf",
"enqueueCNFrec(", theta.
getExpr(),
") { ");
375 TRACE(
"cnf-clauses",
"enqueueCNF call", theta.
getExpr(),
"");
385 TRACE_MSG(
"mycnf",
"enqueueCNFrec[cached] => }");
392 while(thetaExpr.isNot() && thetaExpr[0].isNot()) {
400 if(thetaExpr.isPropLiteral()) {
403 "Must be a literal: theta = "
406 TRACE_MSG(
"mycnf",
"enqueueCNFrec[literal] => }");
407 TRACE(
"cnf-clauses",
"literal with proofs(", theta.
getExpr(),
")");
413 switch(thetaExpr.getKind()) {
416 for(
int i=0; i<thetaExpr.arity(); i++)
418 TRACE_MSG(
"mycnf",
"enqueueCNFrec[AND] => }");
426 i!=iend && cnf; i++) {
427 if(!(*i).isPropLiteral())
431 vector<Theorem> thms;
432 vector<unsigned int> changed;
439 changed.push_back(cc);
442 if(changed.size() > 0) {
448 TRACE_MSG(
"mycnf",
"enqueueCNFrec[cnf] => }");
454 const Expr& t0 = thetaExpr[0];
455 const Expr& t1 = thetaExpr[1];
461 }
else if(thetaExpr[0].isPropLiteral()) {
471 if(thetaExpr[0].isPropLiteral() && thetaExpr[1].isPropLiteral()
472 && thetaExpr[2].isPropLiteral()) {
474 vector<Theorem> thms;
475 vector<unsigned int> changed;
476 for(
int c=0, cend=thetaExpr.arity(); c<cend; ++c) {
482 changed.push_back(c);
485 if(changed.size() > 0) {
493 "enqueueCNFrec [ITE over literals]\n thm = "
510 TRACE(
"cnf-clauses",
"enqueueCNFrec call[cache hit]:(",
513 TRACE_MSG(
"mycnf",
"enqueueCNFrec[cached] => }");
522 TRACE(
"mycnf",
"enqueueCNFrec: varIntroSkolem => ", result.
getExpr(),
528 TRACE(
"mycnf",
"enqueueCNFrec: skolemize => ", result.
getExpr(),
532 "SearchImplBase::CNF(): result = "+result.
toString());
535 "SearchImplBase::CNF(): result = "+result.
toString());
537 "SearchImplBase::CNF(): result = "+result.
toString()
544 TRACE(
"mycnf",
"enqueueCNFrec: theta = ", theta.
getExpr(),
547 TRACE(
"mycnf",
"enqueueCNFrec: var = ", var.getExpr(),
550 DebugAssert(var.isAbsLiteral(),
"var = "+var.getExpr().toString());
555 TRACE_MSG(
"mycnf",
"enqueueCNFrec => }");
564 TRACE(
"mycnf",
"applyCNFRules(", thm.
getExpr(),
") { ");
568 "SearchImplBase::applyCNFRules: input must be an iff: " +
569 result.getExpr().toString());
570 Expr lhs = result.getLHS();
571 Expr rhs = result.getRHS();
573 "SearchImplBase::applyCNFRules: rhs of input must be literal: " +
574 result.getExpr().toString());
577 while(result.getLHS().isNot())
580 rhs = result.getRHS();
586 TRACE_MSG(
"mycnf",
"applyCNFRules[temp cache] => }");
591 if(lhs.isPropLiteral()) {
592 if(!lhs.isAbsLiteral()) {
597 "applyCNFRules [literal lhs]\n result = "
603 "applyCNFRules [literal lhs]\n thm = "
611 vector<unsigned> changed;
612 vector<Theorem> substitutions;
614 for(
Expr::iterator j = lhs.begin(), jend = lhs.end(); j!=jend; ++c,++j) {
615 const Expr& phi = *j;
624 "SearchImplBase::applyCNFRules: result = " +
627 "SearchImplBase::applyCNFRules:\n phi = " +
629 +
"\n\n phiIffVar = " + phiIffVar.
toString());
631 "SearchImplBase::applyCNFRules: phiIffVar = " +
633 changed.push_back(c);
634 substitutions.push_back(phiIffVar);
638 if(changed.size() > 0) {
645 switch(result.getLHS().getKind()) {
663 "SearchImplBase::applyCNFRules: "
664 "the input operator must be and|or|iff|imp|ite\n result = " +
665 result.getLHS().toString());
679 for(
int i=0, iend=clauses.
getExpr().
arity(); i<iend; ++i) {
689 if(!e.
isOr())
return false;
693 cnf = (*i).isAbsLiteral();
701 if(!e.
isOr())
return false;
705 cnf = (*i).isPropLiteral();
713 TRACE(
"isGoodSplitter",
"isGoodSplitter(", e,
") {");
717 TRACE(
"isGoodSplitter",
"isGoodSplitter => ", res?
"true" :
"false",
" }");
730 "SearchImplBase::addToCNFCache: input must be an iff: " +
751 TRACE(
"mycnf",
"findInCNFCache(", e,
") { ");
757 phi = phi[0]; numNegs++;
766 "SearchImplBase::findInCNFCache: thm must be an iff: " +
772 if(numNegs % 2 != 0) {
776 for(; numNegs > 0; numNegs-=2) {
782 TRACE(
"mycnf",
"findInCNFCache => ", thm.
getExpr(),
" }");
785 TRACE_MSG(
"mycnf",
"findInCNFCache => null }");
805 TRACE(
"replaceITE",
"replaceITE(", e,
") { ");
811 TRACE(
"replaceITE",
"replaceITE[cached] => ", (*i).second,
" }");
844 TRACE(
"replaceITE",
"replaceITE => ", res,
" }");
iterator begin() const
Begin iterator.
API to to a generic proof search engine.
virtual Theorem andCNFRule(const Theorem &thm)=0
AND(x1,...,xn) <=> v |- CNF[AND(x1,...,xn) <=> v].
Data structure of expressions in CVC3.
virtual Theorem negIntro(const Expr ¬_a, const Theorem &pfFalse)=0
Negation introduction: .
TheoremManager * getTM() const
virtual Theorem impCNFRule(const Theorem &thm)=0
(x1 => x2) <=> v |- CNF[(x1 => x2) <=> v]
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Representation of a DP-suggested splitter.
void erase(const Expr &e)
const CLFlags & getFlags() const
void enqueueFact(const Theorem &e)
Enqueue a new fact.
TheoryCore::CoreSatAPI * d_coreSatAPI_implBase
virtual Theorem iteCNFRule(const Theorem &thm)=0
ITE(c, x1, x2) <=> v |- CNF[ITE(c, x1, x2) <=> v].
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.
void registerCoreSatAPI(CoreSatAPI *coreSatAPI)
Register a SatAPI for TheoryCore.
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 Theorem assumpRule(const Expr &a, int scope=-1)=0
virtual Proof getProof()
Returns the proof term for the last proven query.
void setUserAssumption(int scope=-1) const
virtual Theorem reflexivityRule(const Expr &a)=0
#define DebugAssert(cond, str)
Theorem rewriteLiteral(const Expr &e)
Called by search engine.
Description: Counters and flags for collecting run-time statistics.
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.
CommonProofRules * d_commonRules
Common proof rules.
virtual void addLemma(const Theorem &thm, int priority, bool atBottomScope)
Add a new lemma derived by theory core.
CDMap< Expr, bool > d_enqueueCNFCache
Cache for enqueueCNF()
virtual Theorem rewriteNotNot(const Expr &e)=0
==> NOT NOT e IFF e, takes !!e
Theorem replaceITE(const Expr &e)
Replaces ITE subexpressions in e with variables.
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
CDMap< Expr, Theorem > d_cnfCache
Backtracking cache for the CNF generator.
bool isPropClause(const Expr &e)
Check if e is a propositional clause.
SearchEngineRules * d_rules
Proof rules for the search engine.
Abstract proof rules interface to the simple search engine.
#define TRACE_MSG(flag, msg)
virtual ~CoreSatAPI_implBase()
Abstract API to the proof search engine.
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.
virtual Theorem addAssumption(const Expr &assump)
Add an assumption to the set of assumptions in the current context.
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.
ExprTransform * getExprTrans() const
void setQuantLevel(unsigned level)
Set the quantification level for this theorem.
virtual Theorem substitutivityRule(const Expr &e, const Theorem &thm)=0
Optimized case for expr with one child.
std::string toString() const
CDMap< Expr, Theorem > d_assumptions
Maintain the list of current assumptions (user asserts and splitters) for getAssumptions().
virtual Theorem iffToClauses(const Theorem &iff)=0
e1 <=> e2 |- (NOT e1 OR e2) AND (e1 OR NOT e2)
std::string toString() const
Print the expression to a string.
virtual Theorem orCNFRule(const Theorem &thm)=0
OR(x1,...,xn) <=> v |- CNF[OR(x1,...,xn) <=> v].
virtual std::vector< Theorem > & getSkolemAxioms()=0
virtual void addSplitter(const Expr &e, int priority)
Suggest a splitter to the Sat engine.
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.
StatCounter counter(const std::string &name)
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 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.
std::string int2string(int n)
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 & getRHS() const
bool isAbsLiteral() const
Check if the theorem is a literal.
virtual Theorem iffCNFRule(const Theorem &thm)=0
(x1 <=> x2) <=> v |- CNF[(x1 <=> x2) <=> v]
Interface class for callbacks to SAT from Core.
const Assumptions & getAssumptionsRef() const
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)
virtual void clearSkolemAxioms()=0
Splitter & operator=(const Splitter &s)
Assignment.
bool isPropLiteral() const
PropAtom or negation of PropAtom.
virtual Theorem iteToClauses(const Theorem &ite)=0
ITE(c, f1, f2) |- (NOT c OR f1) AND (c OR f2)
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.
Generic API for Theories plus methods commonly used by theories.
API to to a generic proof search engine (a.k.a. SAT solver)
TheoryCore * theoryCore()
Accessor for TheoryCore.
virtual Theorem transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)=0
(same for IFF)
virtual Theorem iffContrapositive(const Theorem &thm)=0
e1 <=> e2 ==> ~e1 <=> ~e2
bool isAbsLiteral() const
Test if e is an abstract literal.
CoreSatAPI_implBase(SearchImplBase *se)
virtual Theorem proofByContradiction(const Expr &a, const Theorem &pfFalse)=0
Proof by contradiction: .
CDMap< Expr, bool > d_cnfVars
Backtracking set of new variables generated by CNF translator.
const Expr & getLHS() const
virtual Theorem iffMP(const Theorem &e1, const Theorem &e1_iff_e2)=0
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)
void setIntAssumption() const
CDMap< Expr, Theorem > d_replaceITECache
Cache for replaceITE()
virtual Theorem eliminateSkolemAxioms(const Theorem &tFalse, const std::vector< Theorem > &delta)=0
virtual Theorem notNotElim(const Theorem ¬_not_e)=0
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.
const bool * d_ignoreCnfVarsOption
Flag: ignore auxiliary CNF variables when searching for a splitter.
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.
static const Assumptions & emptyAssump()
void addFact(const Theorem &e)
Add a new assertion to the core from the user or a SAT solver. Do NOT use it in a decision procedure;...
virtual Theorem symmetryRule(const Theorem &a1_eq_a2)=0
(same for IFF)
virtual Theorem varIntroSkolem(const Expr &e)=0
Retrun a theorem "|- e = v" for a new Skolem constant v.
Splitter(const Literal &lit)
Constructor.
virtual Theorem andElim(const Theorem &e, int i)=0
TheoryCore * d_core
Access to theory reasoning.
Statistics & getStatistics() const
virtual QueryResult checkValid(const Expr &e, Theorem &result)
Similar to checkValidInternal(), only returns Theorem(e) or Null.
iterator end() const
End iterator.