Search Engine
[Validity Checker]

Collaboration diagram for Search Engine:

Classes

class CVC3::SearchEngine
API to to a generic proof search engine. More...
class CVC3::SearchImplBase
API to to a generic proof search engine (a.k.a. SAT solver). More...
class CVC3::SearchImplBase::SearchImplBase::Splitter
Representation of a DP-suggested splitter. More...
class CVC3::SearchSat
Search engine that connects to a generic SAT reasoning module. More...

Modules

Fast Search Engine
Simple Search Engine
Decision Engine
Decision Engine, used by Search Engine.
Proof Rules for the Search Engines

Functions

SearchEngineRules * CVC3::SearchEngine::createRules ()
Create the trusted component.
CVC3::SearchEngine::SearchEngine (TheoryCore *core)
Constructor.
virtual CVC3::SearchEngine::~SearchEngine ()
Destructor.
virtual const std::string & CVC3::SearchEngine::getName ()=0
Name of this search engine.
CommonProofRules * CVC3::SearchEngine::getCommonRules ()
Accessor for common rules.
TheoryCore * CVC3::SearchEngine::theoryCore ()
Accessor for TheoryCore.
virtual void CVC3::SearchEngine::registerAtom (const Expr &e)=0
Register an atomic formula of interest.
virtual Theorem CVC3::SearchEngine::getImpliedLiteral ()=0
Return next literal implied by last assertion. Null Expr if none.
virtual void CVC3::SearchEngine::push ()=0
Push a checkpoint.
virtual void CVC3::SearchEngine::pop ()=0
Restore last checkpoint.
virtual QueryResult CVC3::SearchEngine::checkValid (const Expr &e, Theorem &result)=0
Checks the validity of a formula in the current context.
virtual QueryResult CVC3::SearchEngine::restart (const Expr &e, Theorem &result)=0
Reruns last check with e as an additional assumption.
virtual void CVC3::SearchEngine::returnFromCheck ()=0
Returns to context immediately before last call to checkValid.
virtual Theorem CVC3::SearchEngine::lastThm ()=0
Returns the result of the most recent valid theorem.
virtual Theorem CVC3::SearchEngine::newUserAssumption (const Expr &e)=0
Generate and add an assumption to the set of assumptions in the current context.
virtual void CVC3::SearchEngine::getUserAssumptions (std::vector< Expr > &assumptions)=0
Get all user assumptions made in this and all previous contexts.
virtual void CVC3::SearchEngine::getInternalAssumptions (std::vector< Expr > &assumptions)=0
Get assumptions made internally in this and all previous contexts.
virtual void CVC3::SearchEngine::getAssumptions (std::vector< Expr > &assumptions)=0
Get all assumptions made in this and all previous contexts.
virtual bool CVC3::SearchEngine::isAssumption (const Expr &e)=0
Check if the formula has already been assumed previously.
virtual void CVC3::SearchEngine::getCounterExample (std::vector< Expr > &assertions, bool inOrder=true)=0
Will return the set of assertions which make the queried formula false.
virtual Proof CVC3::SearchEngine::getProof ()=0
Returns the proof term for the last proven query.
void CVC3::SearchEngine::getConcreteModel (ExprMap< Expr > &m)
Build a concrete Model (assign values to variables), should only be called after a query which returns INVALID.
bool CVC3::SearchEngine::tryModelGeneration (Theorem &thm)
Try to build a concrete Model (assign values to variables), should only be called after a query which returns UNKNOWN. Returns a theorem if inconsistent.
virtual FormulaValue CVC3::SearchEngine::getValue (const CVC3::Expr &e)=0
Literal CVC3::SearchImplBase::newLiteral (const Expr &e)
Construct a Literal out of an Expr or return an existing one.
Theorem CVC3::SearchImplBase::simplify (const Theorem &e)
Our version of simplifier: take Theorem(e), apply simplifier to get Theorem(e==e'), return Theorem(e').
virtual void CVC3::SearchImplBase::addLiteralFact (const Theorem &thm)=0
Notify the search engine about a new literal fact.
virtual void CVC3::SearchImplBase::addNonLiteralFact (const Theorem &thm)=0
Notify the search engine about a new non-literal fact.
void CVC3::SearchImplBase::addCNFFact (const Theorem &thm, bool fromCore=false)
Add a new fact to the search engine bypassing CNF converter.
int CVC3::SearchImplBase::getBottomScope ()
bool CVC3::SearchImplBase::isClause (const Expr &e)
Check if e is a clause (a literal, or a disjunction of literals).
bool CVC3::SearchImplBase::isPropClause (const Expr &e)
Check if e is a propositional clause.
bool CVC3::SearchImplBase::isCNFVar (const Expr &e)
Check whether e is a fresh variable introduced by the CNF converter.
bool CVC3::SearchImplBase::isGoodSplitter (const Expr &e)
Check if a splitter is required for completeness.
void CVC3::SearchImplBase::enqueueCNF (const Theorem &theta)
Translate theta to CNF and enqueue the new clauses.
void CVC3::SearchImplBase::enqueueCNFrec (const Theorem &theta)
Recursive version of enqueueCNF().
void CVC3::SearchImplBase::applyCNFRules (const Theorem &e)
FIXME: write a comment.
void CVC3::SearchImplBase::addToCNFCache (const Theorem &thm)
Cache a theorem phi <=> v by phi, where v is a literal.
Theorem CVC3::SearchImplBase::findInCNFCache (const Expr &e)
Find a theorem phi <=> v by phi, where v is a literal.
Theorem CVC3::SearchImplBase::replaceITE (const Expr &e)
Replaces ITE subexpressions in e with variables.
int CVC3::SearchImplBase::scopeLevel ()
Return the current scope level (for convenience).
CVC3::SearchImplBase::SearchImplBase (TheoryCore *core)
Constructor.
virtual CVC3::SearchImplBase::~SearchImplBase ()
Destructor.
virtual void CVC3::SearchImplBase::registerAtom (const Expr &e)
Register an atomic formula of interest.
virtual Theorem CVC3::SearchImplBase::getImpliedLiteral ()
Return next literal implied by last assertion. Null Expr if none.
virtual void CVC3::SearchImplBase::push ()
Push a checkpoint.
virtual void CVC3::SearchImplBase::pop ()
Restore last checkpoint.
virtual QueryResult CVC3::SearchImplBase::checkValidInternal (const Expr &e)=0
Checks the validity of a formula in the current context.
virtual QueryResult CVC3::SearchImplBase::checkValid (const Expr &e, Theorem &result)
Similar to checkValidInternal(), only returns Theorem(e) or Null.
virtual QueryResult CVC3::SearchImplBase::restartInternal (const Expr &e)=0
Reruns last check with e as an additional assumption.
virtual QueryResult CVC3::SearchImplBase::restart (const Expr &e, Theorem &result)
Reruns last check with e as an additional assumption.
void CVC3::SearchImplBase::returnFromCheck ()
Returns to context immediately before last call to checkValid.
virtual Theorem CVC3::SearchImplBase::lastThm ()
Returns the result of the most recent valid theorem.
Theorem CVC3::SearchImplBase::newUserAssumption (const Expr &e)
Generate and add a new assertion to the set of assertions in the current context. This should only be used by class VCL in assertFormula().
virtual Theorem CVC3::SearchImplBase::newIntAssumption (const Expr &e)
Add a new internal asserion.
void CVC3::SearchImplBase::newIntAssumption (const Theorem &thm)
Helper for above function.
void CVC3::SearchImplBase::getUserAssumptions (std::vector< Expr > &assumptions)
Get all assumptions made in this and all previous contexts.
void CVC3::SearchImplBase::getInternalAssumptions (std::vector< Expr > &assumptions)
Get assumptions made internally in this and all previous contexts.
virtual void CVC3::SearchImplBase::getAssumptions (std::vector< Expr > &assumptions)
Get all assumptions made in this and all previous contexts.
virtual bool CVC3::SearchImplBase::isAssumption (const Expr &e)
Check if the formula has been assumed.
void CVC3::SearchImplBase::addFact (const Theorem &thm)
Add a new fact to the search engine from the core.
virtual void CVC3::SearchImplBase::addSplitter (const Expr &e, int priority)
Suggest a splitter to the SearchEngine.
virtual void CVC3::SearchImplBase::getCounterExample (std::vector< Expr > &assertions, bool inOrder=true)
Will return the set of assertions which make the queried formula false.
virtual Proof CVC3::SearchImplBase::getProof ()
Returns the proof term for the last proven query.
virtual const Assumptions & CVC3::SearchImplBase::getAssumptionsUsed ()
Returns the set of assumptions used in the proof. It should be a subset of getAssumptions().
void CVC3::SearchImplBase::processResult (const Theorem &res, const Expr &e)
Process result of checkValid.
virtual FormulaValue CVC3::SearchImplBase::getValue (const CVC3::Expr &e)

Variables

TheoryCore * CVC3::SearchEngine::d_core
Access to theory reasoning.
CommonProofRules * CVC3::SearchEngine::d_commonRules
Common proof rules.
SearchEngineRules * CVC3::SearchEngine::d_rules
Proof rules for the search engine.
VariableManager * CVC3::SearchImplBase::d_vm
Variable manager for classes Variable and Literal.
CDO< int > CVC3::SearchImplBase::d_bottomScope
The bottom-most scope for the current call to checkSAT (where conflict clauses are still valid).
TheoryCore::CoreSatAPI * CVC3::SearchImplBase::d_coreSatAPI_implBase
CDList< Splitter > CVC3::SearchImplBase::d_dpSplitters
Backtracking ordered set of DP-suggested splitters.
Theorem CVC3::SearchImplBase::d_lastValid
Theorem from the last successful checkValid call. It is used by getProof and getAssumptions.
ExprHashMap< bool > CVC3::SearchImplBase::d_lastCounterExample
Assumptions from the last unsuccessful checkValid call. These are used by getCounterExample.
CDMap< Expr, Theorem > CVC3::SearchImplBase::d_assumptions
Maintain the list of current assumptions (user asserts and splitters) for getAssumptions().
CDMap< Expr, Theorem > CVC3::SearchImplBase::d_cnfCache
Backtracking cache for the CNF generator.
CDMap< Expr, bool > CVC3::SearchImplBase::d_cnfVars
Backtracking set of new variables generated by CNF translator.
const bool * CVC3::SearchImplBase::d_cnfOption
Command line flag whether to convert to CNF.
const bool * CVC3::SearchImplBase::d_ifLiftOption
Flag: whether to convert term ITEs into CNF.
const bool * CVC3::SearchImplBase::d_ignoreCnfVarsOption
Flag: ignore auxiliary CNF variables when searching for a splitter.
const bool * CVC3::SearchImplBase::d_origFormulaOption
Flag: Preserve the original formula with +cnf (for splitter heuristics).

CNF Caches

These caches are for subexpressions of the translated formula phi, to avoid expanding phi into a tree. We cannot use d_cnfCache for that, since it is effectively non-backtracking, and we do not know if a subexpression of phi was translated at the current level, or at some other (inactive) branch of the decision tree.

CDMap< Expr, bool > CVC3::SearchImplBase::d_enqueueCNFCache
Cache for enqueueCNF().
CDMap< Expr, bool > CVC3::SearchImplBase::d_applyCNFRulesCache
Cache for applyCNFRules().
CDMap< Expr, Theorem > CVC3::SearchImplBase::d_replaceITECache
Cache for replaceITE().

Detailed Description

The search engine includes Boolean reasoning and coordinates with theory reasoning. It consists of a generic abstract API (class SearchEngine) and subclasses implementing concrete instances of search engines.

Function Documentation

SearchEngineRules * SearchEngine::createRules ( ) [protected, inherited]

Create the trusted component.

This function is defined in search_theorem_producer.cpp

Definition at line 41 of file search_theorem_producer.cpp.

References CVC3::SearchEngine::d_core, and CVC3::TheoryCore::getTM().

Referenced by CVC3::SearchEngine::SearchEngine().

SearchEngine::SearchEngine ( TheoryCore * core ) [inherited]

Constructor.

Definition at line 34 of file search.cpp.

References CVC3::SearchEngine::createRules(), and CVC3::SearchEngine::d_rules.

SearchEngine::~SearchEngine ( ) [virtual, inherited]

Destructor.

Definition at line 43 of file search.cpp.

References CVC3::SearchEngine::d_rules.

virtual const std::string& CVC3::SearchEngine::getName ( ) [pure virtual, inherited]

Name of this search engine.

Implemented in CVC3::SearchEngineFast, CVC3::SearchSat, and CVC3::SearchSimple.

Referenced by CVC3::VCL::reprocessFlags().

CommonProofRules* CVC3::SearchEngine::getCommonRules ( ) [inline, inherited]

Accessor for common rules.

Definition at line 82 of file search.h.

References CVC3::SearchEngine::d_commonRules.

Referenced by CVC3::VCL::deriveClosure(), and CVC3::VCL::query().

TheoryCore* CVC3::SearchEngine::theoryCore ( ) [inline, inherited]

Accessor for TheoryCore.

Definition at line 85 of file search.h.

References CVC3::SearchEngine::d_core.

Referenced by CVC3::SearchSat::addLemma(), CVC3::SearchSat::assertLit(), CVC3::CoreSatAPI_implBase::check(), CVC3::SearchImplBase::newIntAssumption(), CVC3::SearchSatTheoryAPI::outOfResources(), and CVC3::SearchSatCNFCallback::registerAtom().

virtual void CVC3::SearchEngine::registerAtom ( const Expr & e ) [pure virtual, inherited]

Register an atomic formula of interest.

Registered atoms are tracked by the decision procedures. If one of them is deduced to be true or false, it is added to a list of implied literals. Implied literals can be retrieved with the getImpliedLiteral function

Implemented in CVC3::SearchImplBase, and CVC3::SearchSat.

Referenced by CVC3::VCL::registerAtom().

virtual Theorem CVC3::SearchEngine::getImpliedLiteral ( ) [pure virtual, inherited]

Return next literal implied by last assertion. Null Expr if none.

Returned literals are either registered atomic formulas or their negation

Implemented in CVC3::SearchImplBase, and CVC3::SearchSat.

Referenced by CVC3::VCL::getImpliedLiteral().

virtual void CVC3::SearchEngine::push ( ) [pure virtual, inherited]

Push a checkpoint.

Implemented in CVC3::SearchImplBase, and CVC3::SearchSat.

Referenced by CVC3::VCL::checkTCC(), CVC3::SearchEngine::getConcreteModel(), CVC3::VCL::push(), CVC3::VCL::tryModelGeneration(), and CVC3::SearchEngine::tryModelGeneration().

virtual void CVC3::SearchEngine::pop ( ) [pure virtual, inherited]

Restore last checkpoint.

Implemented in CVC3::SearchImplBase, and CVC3::SearchSat.

Referenced by CVC3::VCL::checkTCC(), CVC3::SearchEngine::getConcreteModel(), CVC3::VCL::pop(), CVC3::VCL::popto(), CVC3::VCL::tryModelGeneration(), and CVC3::SearchEngine::tryModelGeneration().

virtual QueryResult CVC3::SearchEngine::checkValid	(	const Expr &	e,
		Theorem &	result
	)			`[pure virtual, inherited]`

Checks the validity of a formula in the current context.

If the query is valid, it returns VALID, the result parameter contains the corresponding theorem, and the scope and context are the same as when called. If it returns INVALID, the context will be one which falsifies the query. If it returns UNKNOWN, the context will falsify the query, but the context may be inconsistent. Finally, if it returns ABORT, the context will be one which satisfies as much as possible.

Parameters:

	e	the formula to check.
	result	the resulting theorem, if the formula is valid.

Implemented in CVC3::SearchImplBase, and CVC3::SearchSat.

Referenced by CVC3::VCL::checkTCC(), CVC3::SearchEngine::getConcreteModel(), CVC3::VCL::query(), and CVC3::SearchEngine::tryModelGeneration().

virtual QueryResult CVC3::SearchEngine::restart	(	const Expr &	e,
		Theorem &	result
	)			`[pure virtual, inherited]`

Reruns last check with e as an additional assumption.

This method should only be called after a query which is invalid.

Parameters:

	e	the additional assumption
	result	the resulting theorem, if the query is valid.

Implemented in CVC3::SearchImplBase, and CVC3::SearchSat.

Referenced by CVC3::VCL::checkContinue(), and CVC3::VCL::restart().

virtual void CVC3::SearchEngine::returnFromCheck ( ) [pure virtual, inherited]

Returns to context immediately before last call to checkValid.

This method should only be called after a query which returns something other than VALID.

Implemented in CVC3::SearchImplBase, and CVC3::SearchSat.

Referenced by CVC3::VCL::returnFromCheck().

virtual Theorem CVC3::SearchEngine::lastThm ( ) [pure virtual, inherited]

Returns the result of the most recent valid theorem.

Returns Null Theorem if last call was not valid

Implemented in CVC3::SearchImplBase, and CVC3::SearchSat.

Referenced by CVC3::VCL::getAssumptionsUsed(), CVC3::SearchEngine::getConcreteModel(), and CVC3::SearchEngine::tryModelGeneration().

virtual Theorem CVC3::SearchEngine::newUserAssumption ( const Expr & e ) [pure virtual, inherited]

Generate and add an assumption to the set of assumptions in the current context.

By default, the assumption is added at the current scope. The default can be overridden by specifying the scope parameter.

Implemented in CVC3::SearchImplBase, and CVC3::SearchSat.

Referenced by CVC3::VCL::assertFormula().

virtual void CVC3::SearchEngine::getUserAssumptions ( std::vector< Expr > & assumptions ) [pure virtual, inherited]

Get all user assumptions made in this and all previous contexts.

User assumptions are created either by calls to newUserAssumption or a call to checkValid. In the latter case, the negated query is added as an assumption.

Parameters:

assumptions

should be empty on entry.

Implemented in CVC3::SearchImplBase, and CVC3::SearchSat.

Referenced by CVC3::VCL::getUserAssumptions().

virtual void CVC3::SearchEngine::getInternalAssumptions ( std::vector< Expr > & assumptions ) [pure virtual, inherited]

Get assumptions made internally in this and all previous contexts.

Internal assumptions are literals assumed by the sat solver.

Parameters:

assumptions

should be empty on entry.

Implemented in CVC3::SearchImplBase, and CVC3::SearchSat.

Referenced by CVC3::VCL::getInternalAssumptions().

virtual void CVC3::SearchEngine::getAssumptions ( std::vector< Expr > & assumptions ) [pure virtual, inherited]

Get all assumptions made in this and all previous contexts.

Parameters:

assumptions

should be an empty vector which will be filled \ with the assumptions

Implemented in CVC3::SearchImplBase, and CVC3::SearchSat.

Referenced by CVC3::VCL::getAssumptions(), and CVC3::SearchEngine::getConcreteModel().

virtual bool CVC3::SearchEngine::isAssumption ( const Expr & e ) [pure virtual, inherited]

Check if the formula has already been assumed previously.

Implemented in CVC3::SearchEngineFast, CVC3::SearchImplBase, and CVC3::SearchSat.

virtual void CVC3::SearchEngine::getCounterExample	(	std::vector< Expr > &	assertions,
		bool	inOrder = `true`
	)			`[pure virtual, inherited]`

Will return the set of assertions which make the queried formula false.

This method should only be called after an query which returns INVALID. It will try to return the simplest possible set of assertions which are sufficient to make the queried expression false.

Parameters:

	assertions	should be empty on entry.
	inOrder	if true, returns the assertions in the order they were asserted. This is slightly more expensive than inOrder = false.

Implemented in CVC3::SearchImplBase, and CVC3::SearchSat.

Referenced by CVC3::VCL::checkContinue(), and CVC3::VCL::getCounterExample().

virtual Proof CVC3::SearchEngine::getProof ( ) [pure virtual, inherited]

Returns the proof term for the last proven query.

It should be called only after a query which returns VALID. In any other case, it returns Null.

Implemented in CVC3::SearchImplBase, and CVC3::SearchSat.

Referenced by CVC3::VCL::getProof().

void SearchEngine::getConcreteModel ( ExprMap< Expr > & m ) [inherited]

Build a concrete Model (assign values to variables), should only be called after a query which returns INVALID.

Definition at line 82 of file search.cpp.

References CVC3::TheoryCore::buildModel(), CVC3::SearchEngine::checkValid(), CVC3::TheoryCore::collectBasicVars(), CVC3::SearchEngine::d_core, CVC3::Theory::falseExpr(), CVC3::SearchEngine::getAssumptions(), CVC3::Theory::getEM(), CVC3::Theorem::getLeafAssumptions(), CVC3::TheoryCore::inconsistentThm(), CVC3::SearchEngine::lastThm(), CVC3::SearchEngine::pop(), CVC3::SearchEngine::push(), CVC3::RAW_LIST, CVC3::TheoryCore::refineCounterExample(), CVC3::Expr::toString(), CVC3::TRACE, and CVC3::VALID.

Referenced by CVC3::VCL::getConcreteModel().

bool SearchEngine::tryModelGeneration ( Theorem & thm ) [inherited]

Try to build a concrete Model (assign values to variables), should only be called after a query which returns UNKNOWN. Returns a theorem if inconsistent.

Definition at line 48 of file search.cpp.

References CVC3::TheoryCore::buildModel(), CVC3::SearchEngine::checkValid(), CVC3::TheoryCore::collectBasicVars(), CVC3::SearchEngine::d_core, CVC3::Theory::falseExpr(), CVC3::SearchEngine::lastThm(), CVC3::SearchEngine::pop(), CVC3::SearchEngine::push(), CVC3::TheoryCore::refineCounterExample(), and CVC3::VALID.

Referenced by CVC3::VCL::tryModelGeneration().

virtual FormulaValue CVC3::SearchEngine::getValue ( const CVC3::Expr & e ) [pure virtual, inherited]

Implemented in CVC3::SearchImplBase, and CVC3::SearchSat.

Referenced by CVC3::VCL::value().

Literal CVC3::SearchImplBase::newLiteral ( const Expr & e ) [inline, protected, inherited]

Construct a Literal out of an Expr or return an existing one.

Definition at line 120 of file search_impl_base.h.

References CVC3::SearchImplBase::d_vm.

Referenced by CVC3::SearchEngineFast::addLiteralFact(), CVC3::SearchEngineFast::addNonLiteralFact(), CVC3::SearchImplBase::addSplitter(), CVC3::SearchEngineFast::addSplitter(), CVC3::SearchEngineFast::newIntAssumption(), CVC3::Circuit::propagate(), CVC3::SearchEngineFast::recordFact(), CVC3::SearchEngineFast::split(), CVC3::SearchEngineFast::traceConflict(), and CVC3::SearchEngineFast::unitPropagation().

Theorem CVC3::SearchImplBase::simplify ( const Theorem & e ) [inline, protected, inherited]

Our version of simplifier: take Theorem(e), apply simplifier to get Theorem(e==e'), return Theorem(e').

Definition at line 124 of file search_impl_base.h.

References CVC3::SearchEngine::d_core, CVC3::Theorem::getExpr(), CVC3::Theory::iffMP(), and CVC3::TheoryCore::simplify().

Referenced by CVC3::SearchEngineFast::bcp(), CVC3::SearchEngineFast::checkValidMain(), and CVC3::SearchSimple::checkValidRec().

virtual void CVC3::SearchImplBase::addLiteralFact ( const Theorem & thm ) [protected, pure virtual, inherited]

Notify the search engine about a new literal fact.

It should be called by SearchEngine::addFact() only. Must be implemented by the subclasses of SearchEngine.

IMPORTANT: do not call addFact() from this function; use enqueueFact() or setInconsistent() instead.

Implemented in CVC3::SearchEngineFast, and CVC3::SearchSimple.

Referenced by CVC3::SearchImplBase::addCNFFact(), and CVC3::DecisionEngine::pushDecision().

virtual void CVC3::SearchImplBase::addNonLiteralFact ( const Theorem & thm ) [protected, pure virtual, inherited]

Notify the search engine about a new non-literal fact.

It should be called by SearchEngine::addFact() only. Must be implemented by the subclasses of SearchEngine.

IMPORTANT: do not call addFact() from this function; use enqueueFact() or setInconsistent() instead.

Implemented in CVC3::SearchEngineFast, and CVC3::SearchSimple.

Referenced by CVC3::SearchImplBase::addCNFFact().

void SearchImplBase::addCNFFact	(	const Theorem &	thm,
		bool	fromCore = `false`
	)			`[protected, inherited]`

Add a new fact to the search engine bypassing CNF converter.

Calls either addLiteralFact() or addNonLiteralFact() appropriately, and converts to CNF when d_cnfOption is set. If fromCore==true, this fact already comes from the core, and doesn't need to be reported back to the core.

Definition at line 218 of file search_impl_base.cpp.

References CVC3::SearchImplBase::addLiteralFact(), CVC3::SearchImplBase::addNonLiteralFact(), CVC3::SearchEngine::d_core, CVC3::TheoryCore::enqueueFact(), CVC3::Theorem::getExpr(), CVC3::Theorem::isAbsLiteral(), CVC3::TRACE, and TRACE_MSG.

Referenced by CVC3::SearchImplBase::addFact(), CVC3::SearchImplBase::applyCNFRules(), CVC3::SearchImplBase::enqueueCNF(), and CVC3::SearchImplBase::enqueueCNFrec().

int CVC3::SearchImplBase::getBottomScope ( ) [inline, inherited]

Definition at line 153 of file search_impl_base.h.

References CVC3::SearchImplBase::d_bottomScope.

bool SearchImplBase::isClause ( const Expr & e ) [inherited]

Check if e is a clause (a literal, or a disjunction of literals).

Definition at line 687 of file search_impl_base.cpp.

References CVC3::Expr::begin(), CVC3::Expr::end(), CVC3::Expr::isAbsLiteral(), and CVC3::Expr::isOr().

bool SearchImplBase::isPropClause ( const Expr & e ) [inherited]

Check if e is a propositional clause.

See also:: isPropAtom()

Definition at line 699 of file search_impl_base.cpp.

References CVC3::Expr::begin(), CVC3::Expr::end(), CVC3::Expr::isOr(), and CVC3::Expr::isPropLiteral().

bool CVC3::SearchImplBase::isCNFVar ( const Expr & e ) [inline, inherited]

Check whether e is a fresh variable introduced by the CNF converter.

Search engines do not need to split on those variables in order to be complete

Definition at line 165 of file search_impl_base.h.

References CVC3::CDMap< Key, Data, HashFcn >::count(), and CVC3::SearchImplBase::d_cnfVars.

Referenced by CVC3::SearchImplBase::isGoodSplitter().

bool SearchImplBase::isGoodSplitter ( const Expr & e ) [inherited]

Check if a splitter is required for completeness.

Currently, it checks that 'e' is not an auxiliary CNF variable

Definition at line 711 of file search_impl_base.cpp.

References CVC3::SearchImplBase::d_ignoreCnfVarsOption, CVC3::SearchImplBase::isCNFVar(), CVC3::Expr::isNot(), and CVC3::TRACE.

Referenced by CVC3::SearchEngineFast::findSplitter(), and CVC3::DecisionEngine::findSplitterRec().

void SearchImplBase::enqueueCNF ( const Theorem & theta ) [private, inherited]

Translate theta to CNF and enqueue the new clauses.

Definition at line 360 of file search_impl_base.cpp.

References CVC3::SearchImplBase::addCNFFact(), CVC3::SearchImplBase::d_origFormulaOption, CVC3::SearchImplBase::enqueueCNFrec(), CVC3::TRACE, and TRACE_MSG.

Referenced by CVC3::SearchImplBase::addFact().

void SearchImplBase::enqueueCNFrec ( const Theorem & theta ) [private, inherited]

Recursive version of enqueueCNF().

Definition at line 371 of file search_impl_base.cpp.

References CVC3::SearchImplBase::addCNFFact(), CVC3::SearchImplBase::addToCNFCache(), CVC3::AND, CVC3::CommonProofRules::andElim(), CVC3::SearchImplBase::applyCNFRules(), CVC3::Expr::arity(), CVC3::CDMap< Key, Data, HashFcn >::count(), CVC3::SearchImplBase::d_cnfVars, CVC3::SearchEngine::d_commonRules, CVC3::SearchImplBase::d_enqueueCNFCache, CVC3::SearchImplBase::d_ifLiftOption, CVC3::SearchEngine::d_rules, DebugAssert, CVC3::SearchImplBase::findInCNFCache(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Theorem::getRHS(), CVC3::Theorem::getScope(), CVC3::IFF, CVC3::CommonProofRules::iffMP(), CVC3::int2string(), CVC3::Expr::isAbsLiteral(), CVC3::Theorem::isAbsLiteral(), CVC3::Expr::isAnd(), CVC3::Theorem::isNull(), CVC3::Expr::isPropLiteral(), CVC3::Theorem::isRewrite(), CVC3::ITE, CVC3::SearchEngineRules::iteToClauses(), CVC3::CommonProofRules::notNotElim(), CVC3::OR, CVC3::SearchImplBase::replaceITE(), CVC3::SearchImplBase::scopeLevel(), CVC3::CommonProofRules::substitutivityRule(), CVC3::CommonProofRules::symmetryRule(), CVC3::Theorem::toString(), CVC3::Expr::toString(), CVC3::TRACE, TRACE_MSG, CVC3::CommonProofRules::transitivityRule(), and CVC3::CommonProofRules::varIntroSkolem().

Referenced by CVC3::SearchImplBase::enqueueCNF().

void SearchImplBase::applyCNFRules ( const Theorem & thm ) [private, inherited]

FIXME: write a comment.

Parameters:

thm

is the input of the form phi <=> v

Definition at line 563 of file search_impl_base.cpp.

References CVC3::SearchImplBase::addCNFFact(), CVC3::SearchImplBase::addToCNFCache(), CVC3::AND, CVC3::SearchEngineRules::andCNFRule(), CVC3::CommonProofRules::andElim(), CVC3::Expr::arity(), CVC3::SearchImplBase::d_applyCNFRulesCache, CVC3::SearchEngine::d_commonRules, CVC3::SearchEngine::d_rules, DebugAssert, CVC3::CDMap< Key, Data, HashFcn >::end(), CVC3::CDMap< Key, Data, HashFcn >::find(), CVC3::SearchImplBase::findInCNFCache(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Theorem::getRHS(), CVC3::IFF, CVC3::SearchEngineRules::iffCNFRule(), CVC3::CommonProofRules::iffContrapositive(), CVC3::SearchEngineRules::iffToClauses(), CVC3::SearchEngineRules::impCNFRule(), CVC3::IMPLIES, CVC3::Expr::isAbsLiteral(), CVC3::Expr::isAnd(), CVC3::Theorem::isNull(), CVC3::Expr::isPropLiteral(), CVC3::Theorem::isRewrite(), CVC3::ITE, CVC3::SearchEngineRules::iteCNFRule(), CVC3::OR, CVC3::SearchEngineRules::orCNFRule(), CVC3::SearchImplBase::replaceITE(), CVC3::CommonProofRules::substitutivityRule(), CVC3::CommonProofRules::symmetryRule(), CVC3::Theorem::toString(), CVC3::Expr::toString(), CVC3::TRACE, TRACE_MSG, CVC3::CommonProofRules::transitivityRule(), and CVC3::CommonProofRules::varIntroSkolem().

Referenced by CVC3::SearchImplBase::enqueueCNFrec(), and CVC3::SearchImplBase::replaceITE().

void SearchImplBase::addToCNFCache ( const Theorem & thm ) [private, inherited]

Cache a theorem phi <=> v by phi, where v is a literal.

Definition at line 723 of file search_impl_base.cpp.

References CVC3::CDMap< Key, Data, HashFcn >::count(), CVC3::Statistics::counter(), CVC3::SearchImplBase::d_bottomScope, CVC3::SearchImplBase::d_cnfCache, CVC3::SearchImplBase::d_cnfVars, CVC3::SearchEngine::d_commonRules, CVC3::SearchEngine::d_core, DebugAssert, CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Theorem::getRHS(), CVC3::TheoryCore::getStatistics(), CVC3::CommonProofRules::iffContrapositive(), CVC3::CDMap< Key, Data, HashFcn >::insert(), CVC3::Expr::isNot(), CVC3::Theorem::isRewrite(), CVC3::Expr::toString(), and CVC3::TRACE.

Referenced by CVC3::SearchImplBase::applyCNFRules(), CVC3::SearchImplBase::enqueueCNFrec(), and CVC3::SearchImplBase::replaceITE().

Theorem SearchImplBase::findInCNFCache ( const Expr & e ) [private, inherited]

Find a theorem phi <=> v by phi, where v is a literal.

Returns:: Null Theorem if not found.

Definition at line 750 of file search_impl_base.cpp.

References CVC3::Statistics::counter(), CVC3::SearchImplBase::d_cnfCache, CVC3::SearchEngine::d_commonRules, CVC3::SearchEngine::d_core, DebugAssert, CVC3::CDMap< Key, Data, HashFcn >::end(), CVC3::CDMap< Key, Data, HashFcn >::find(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::TheoryCore::getStatistics(), CVC3::CommonProofRules::iffContrapositive(), CVC3::int2string(), CVC3::Expr::isNot(), CVC3::Theorem::isRewrite(), CVC3::CommonProofRules::rewriteNotNot(), CVC3::Expr::toString(), CVC3::TRACE, TRACE_MSG, and CVC3::CommonProofRules::transitivityRule().

Referenced by CVC3::SearchImplBase::applyCNFRules(), CVC3::SearchImplBase::enqueueCNFrec(), and CVC3::SearchImplBase::replaceITE().

Theorem SearchImplBase::replaceITE ( const Expr & e ) [private, inherited]

Replaces ITE subexpressions in e with variables.

Strategy:

For a given atomic formula phi(ite(c, t1, t2)) which depends on a term ITE, generate an equisatisfiable formula:

phi(x) & ite(c, t1=x, t2=x),

where x is a new variable.

The phi(x) part will be generated by the caller, and our job is to assert the 'ite(c, t1=x, t2=x)', and return a rewrite theorem phi(ite(c, t1, t2)) <=> phi(x).

Definition at line 804 of file search_impl_base.cpp.

References CVC3::SearchImplBase::addToCNFCache(), CVC3::SearchImplBase::applyCNFRules(), CVC3::SearchEngine::d_commonRules, CVC3::SearchEngine::d_core, CVC3::SearchImplBase::d_replaceITECache, CVC3::CDMap< Key, Data, HashFcn >::end(), CVC3::CDMap< Key, Data, HashFcn >::find(), CVC3::SearchImplBase::findInCNFCache(), CVC3::Theorem::getRHS(), CVC3::CommonProofRules::iffMP(), CVC3::Expr::isAbsLiteral(), CVC3::Theorem::isNull(), CVC3::Expr::isPropLiteral(), CVC3::Theorem::isRewrite(), CVC3::CommonProofRules::reflexivityRule(), CVC3::TheoryCore::rewriteLiteral(), CVC3::TRACE, CVC3::CommonProofRules::transitivityRule(), and CVC3::CommonProofRules::varIntroSkolem().

Referenced by CVC3::SearchImplBase::applyCNFRules(), and CVC3::SearchImplBase::enqueueCNFrec().

int CVC3::SearchImplBase::scopeLevel ( ) [inline, protected, inherited]

Return the current scope level (for convenience).

Definition at line 192 of file search_impl_base.h.

References CVC3::SearchEngine::d_core, CVC3::TheoryCore::getCM(), and CVC3::ContextManager::scopeLevel().

SearchImplBase::SearchImplBase ( TheoryCore * core ) [inherited]

Constructor.

Definition at line 107 of file search_impl_base.cpp.

References CVC3::SearchImplBase::d_assumptions, CVC3::SearchImplBase::d_coreSatAPI_implBase, CVC3::SearchEngine::d_rules, CVC3::SearchImplBase::d_vm, CVC3::TheoryCore::getCM(), CVC3::TheoryCore::getFlags(), IF_DEBUG, and CVC3::TheoryCore::registerCoreSatAPI().

SearchImplBase::~SearchImplBase ( ) [virtual, inherited]

Destructor.

Definition at line 132 of file search_impl_base.cpp.

References CVC3::SearchImplBase::d_coreSatAPI_implBase, and CVC3::SearchImplBase::d_vm.

virtual void CVC3::SearchImplBase::registerAtom ( const Expr & e ) [inline, virtual, inherited]

Register an atomic formula of interest.

Registered atoms are tracked by the decision procedures. If one of them is deduced to be true or false, it is added to a list of implied literals. Implied literals can be retrieved with the getImpliedLiteral function

QueryResult SearchImplBase::checkValid	(	const Expr &	e,
		Theorem &	result
	)			`[virtual, inherited]`

QueryResult SearchImplBase::restart	(	const Expr &	e,
		Theorem &	result
	)			`[virtual, inherited]`

void SearchImplBase::addSplitter	(	const Expr &	e,
		int	priority
	)			`[virtual, inherited]`

void SearchImplBase::getCounterExample	(	std::vector< Expr > &	assertions,
		bool	inOrder = `true`
	)			`[virtual, inherited]`

void SearchImplBase::processResult	(	const Theorem &	res,
		const Expr &	e
	)			`[inherited]`

	res	is a proof of FALSE
	e	is the assumption used in the above proof

Search Engine [Validity Checker]

Classes

Modules

Functions

Variables

CNF Caches

Detailed Description

Function Documentation

Variable Documentation

Search Engine
[Validity Checker]