37 d_commonRules(core->getTM()->getRules())
41 if (flg[
"lfsc-mode"].getInt()!= 0){
59 if(!
lastThm().isNull())
throw EvalException(
"Method tryModelGenereation() (or command COUNTERMODEL)\n must be called only after failed QUERY");
93 TRACE(
"model" ,
"Building a concrete model",
"",
"{");
96 (
"Method getConcreteModel() (or command COUNTERMODEL)\n"
97 " must be called only after failed QUERY");
117 (
"Model Creation failed after refining counterexample\n"
118 "due to the following assumptions:\n "
120 +
"\n\nYou might be using an incomplete fragment of the theory");
140 (
"Model Creation failed due to the following assumptions:\n"
142 +
"\n\nYou might be using an incomplete fragment of the theory");
148 TRACE(
"model" ,
"Building a concrete model",
"",
"}");
Data structure of expressions in CVC3.
TheoremManager * getTM() const
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Abstract API to the proof search engine.
void getConcreteModel(ExprMap< Expr > &m)
Build a concrete Model (assign values to variables), should only be called after a query which return...
void getLeafAssumptions(std::vector< Expr > &assumptions, bool negate=false) const
virtual void getAssumptions(std::vector< Expr > &assumptions)=0
Get all assumptions made in this and all previous contexts.
bool tryModelGeneration(Theorem &thm)
Try to build a concrete Model (assign values to variables), should only be called after a query which...
SearchEngineRules * d_rules
Proof rules for the search engine.
Abstract proof rules interface to the simple search engine.
virtual void pop()=0
Restore last checkpoint.
virtual void push()=0
Push a checkpoint.
virtual QueryResult checkValid(const Expr &e, Theorem &result)=0
Checks the validity of a formula in the current context.
virtual ~SearchEngine()
Destructor.
void refineCounterExample()
Calls for other theories to add facts to refine a coutnerexample.
SearchEngine(TheoryCore *core)
Constructor.
std::string toString() const
Print the expression to a string.
void collectBasicVars()
Split compound vars into basic type variables.
const Expr & falseExpr()
Return FALSE Expr.
ExprManager * getEM()
Access to ExprManager.
virtual Theorem lastThm()=0
Returns the result of the most recent valid theorem.
SearchEngineRules * createRules()
Create the trusted component.
Theorem inconsistentThm()
Get the proof of inconsistency for the current context.
const CLFlags & getFlags() const
TheoryCore * d_core
Access to theory reasoning.
void buildModel(ExprMap< Expr > &m)
Calls theory specific computeModel, results are placed in map.