37 : d_em(theoryCore->getEM()),
38 d_theoryCore(theoryCore),
39 d_commonRules(theoryCore->getTM()->getRules()),
40 d_name(name), d_theoryUsed(false) {
48 TRACE(
"model",
"Theory::computeModelTerm(", e,
"): is a variable");
63 vector<Theorem> newChildrenThm;
64 vector<unsigned> changed;
65 for(
int k = 0; k < ar; ++k) {
69 newChildrenThm.push_back(thm);
73 if(changed.size() > 0)
84 kids.push_back(
getTCC(*i));
85 return (kids.size() == 0) ?
trueExpr() :
86 (kids.size() == 1) ? kids[0] :
107 IF_DEBUG(debugger.counter(
"conflicts from DPs")++;)
149 TRACE(
"facts assertFact",
"addSplitter[" +
getName() +
"->](", e,
163 TRACE(
"facts assertFact",
"assignValue["+
getName()+
"](", t,
", "+
166 TRACE(
"facts assertFact",
"assignValue[",
getName(),
"] => }");
171 TRACE(
"facts assertFact",
"assignValue["+
getName()+
"](", thm,
") {");
173 TRACE(
"facts assertFact",
"assignValue[",
getName(),
"] => }");
179 vector<int>::const_iterator k;
180 vector<int>::const_iterator kEnd;
181 for (k = kinds.begin(), kEnd = kinds.end(); k != kEnd; ++k) {
192 vector<int>::const_iterator k;
193 vector<int>::const_iterator kEnd;
194 for (k = kinds.begin(), kEnd = kinds.end(); k != kEnd; ++k) {
196 "kind not registered: "+
getEM()->getKindName(*k)
299 if (thm1.isRefl())
return thm1;
300 const Expr& e1 = thm1.getRHS();
314 if (thm1.
isRefl())
return thm1;
316 if (e1 == e || !e1.
hasFind() ||
339 vector<Theorem> newChildrenThm;
340 vector<unsigned> changed;
341 for(
int k = 0; k < ar; ++k) {
345 newChildrenThm.push_back(thm);
346 changed.push_back(k);
349 if(changed.size() > 0)
372 return (*itccCache).second;
375 TRACE(
"tccs",
"computeTCC["+i->
getName()+
"](", e,
") {");
378 TRACE(
"tccs",
"computeTCC["+i->
getName()+
"] => ", tcc,
" }");
395 if(!res.isNull())
return res;
398 "Theory::getBaseType(): No theory for the type: "
440 vector<Theorem> newChildrenThm;
441 vector<unsigned> changed;
442 for (
int k = 0; k < ar; ++k) {
445 newChildrenThm.push_back(thm);
446 changed.push_back(k);
449 if (changed.size() > 0)
461 for (
int k = 0; k < e.
arity(); ++k) {
476 int k, ar(d.
arity());
478 if (!dEQdsig.isNull()) {
479 const Expr& dsig = dEQdsig.getRHS();
482 if (sigNew == dsig) {
488 if (!repEQsigNew.
isNull()) {
497 for (k = 0; k < ar; ++k) {
498 if (sigNew[k] != dsig[k]) {
530 TRACE(
"model",
"computeModelTerm["+i->
getName()+
"](", e,
") {");
533 TRACE(
"model",
"computeModelTerm[", i->
getName(),
"] => }");
534 DebugAssert(v.size() <= size || v.back() != e,
"Primitive var was pushed on "
535 "the stack in computeModelTerm["+i->
getName()
549 if (e1 == e2)
return true;
550 if (
theoryOf(e2) !=
this)
return false;
562 for (
int k = 0; k < e.
arity(); ++k) {
579 (
"incompatible redefinition of variable "+name+
":\n "
580 "already defined with type: "+t.
toString()
581 +
"\n the new type is: "+type.
toString());
600 throw Exception(
"newVar: expected non-function type");
602 if( !res.lookupType().isNull() ) {
603 throw Exception(
"newVarExpr: redefining a variable " + name);
617 (
"Redefinition of variable "+name+
":\n "
618 "This variable is already defined.");
624 while(t.getExpr().getKind() ==
TYPEDEF) {
625 DebugAssert(t.arity() == 2,
"Bad TYPEDEF: "+t.toString());
633 " is declared with type:\n "
635 +
"\nBut the type of definition is\n "
648 bool computeTransClosure) {
655 (
"Redefinition of variable "+name+
":\n "
656 "already defined with type: "+t.
toString()
657 +
"\n the new type is: "+type.
toString());
671 if (computeTransClosure &&
673 res.setComputeTransClosure();
686 (
"Redefinition of name "+name+
":\n "
687 "already defined with type: "+t.
toString()
688 +
"\n the new type is: "+type.
toString());
701 if ((*type).isNull())
return Op();
712 Expr v(
getEM()->newBoundVarExpr(name, ss.str(), type));
715 "Parse cache invariant violated");
718 "Expected empty cache");
722 "Parse cache invariant violated 2");
729 (*iBoundVarMap).second =
Expr(
RAW_LIST, v, (*iBoundVarMap).second);
733 TRACE(
"vars",
"addBoundVar("+name+
", ", type,
") => "+v.
toString());
749 getEM()->newBoundVarExpr(name, ss.str(), type), def);
753 "Parse cache invariant violated");
756 "Expected empty cache");
760 "Parse cache invariant violated 2");
767 (*iBoundVarMap).second =
Expr(
RAW_LIST, res, (*iBoundVarMap).second);
770 TRACE(
"vars",
"addBoundVar("+name+
", "+type.
toString()+
", ", def,
783 if ((*type).isNull())
return Expr();
795 (
"Redefinition of type variable "+name+
":\n "
796 "This variable is already defined.");
819 if(!predTp.isFunction() || predTp.arity() != 2)
821 (
"Expected unary predicate in the predicate subtype:\n\n "
823 +
"\n\nThe predicate is:\n\n "
825 if(!predTp[1].isBool())
827 (
"Range is not BOOLEAN in the predicate subtype:\n\n "
829 +
"\n\nThe predicate is:\n\n "
844 (
"Subtype predicate could not be proved total in the following type:\n\n "
846 +
"\n\nThe failed TCC is:\n\n "
862 (
"Unable to prove witness for subtype:\n\n "
864 +
"\n\nThe failed condition is:\n\n "
877 (
"Redefinition of type variable "+name+
":\n "
878 "This variable is already defined.");
893 res = (*iBoundVarMap).second;
913 "installID called on existing identifier");
virtual Theorem simplify(const Expr &e)
Simplify a term e and return a Theorem(e==e')
virtual Expr parseExpr(const Expr &e)
Parse the generic expression.
iterator begin() const
Begin iterator.
Theory * d_solver
The theory which has the solver (if any)
TheoryCore * d_theoryCore
Provides the core functionality.
bool leavesAreSimp(const Expr &e)
Test if all i-leaves of e are simplified.
_hash_table::iterator iterator
Data structure of expressions in CVC3.
const Theorem & getFind() const
Theorem typePred(const Expr &e)
Return BOOLEAN type.
void addSplitter(const Expr &e, int priority=0)
Suggest a splitter to the SearchEngine.
bool isLeafIn(const Expr &e1, const Expr &e2)
Test if e1 is an i-leaf in e2.
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
bool isLeaf(const Expr &e)
Test if e is an i-leaf term for the current theory.
virtual void assertEqualities(const Theorem &e)
Handle new equalities (usually asserted through addFact)
virtual void setInconsistent(const Theorem &e)
Make the context inconsistent; The formula proved by e must FALSE.
virtual void setIncomplete(const std::string &reason)
Mark the current decision branch as possibly incomplete.
const CLFlags & getFlags() const
void enqueueFact(const Theorem &e)
Enqueue a new fact.
void setupCC(const Expr &e)
Setup a term for congruence closure (must have sig and rep attributes)
void addToVarDB(const Expr &e)
Adds expression to var database.
bool hasTheory(int kind)
Test whether a kind maps to any theory.
void addToNotify(Theory *i, const Expr &e) const
Add (e,i) to the notify list of this expression.
An exception to be thrown at typecheck error.
iterator find(const Expr &e)
Expr newSymbolExpr(const std::string &s, int kind)
Type newSubtypeExpr(const Expr &pred, const Expr &witness)
Create a new subtype expression.
Expr resolveID(const std::string &name)
Resolve an identifier, for use in parseExprOp()
virtual Expr computeTypePred(const Type &t, const Expr &e)
Theory specific computation of the subtyping predicate for type t applied to the expression e...
void setIncomplete(const std::string &reason)
Mark the branch as incomplete.
void setFind(const Theorem &e) const
Set the find attribute to e.
MS C++ specific settings.
virtual void enqueueFact(const Theorem &e)
Submit a derived fact to the core from a decision procedure.
virtual void addLemma(const Theorem &thm, int priority=0, bool atBottomScope=false)=0
Add a new lemma derived by theory core.
virtual Theorem rewriteAnd(const Expr &e)=0
==> AND(e1,e2) IFF [simplified expr]
ExprMap< Expr > d_tccCache
Cache for tcc's.
virtual void enqueueSE(const Theorem &e)
Check if the current context is inconsistent.
Type lookupType() const
Look up the current type. Do not recursively compute (i.e. may be NULL)
void unregisterTheory(Theory *theory, std::vector< int > &kinds, bool hasSolver)
Unregister a theory.
void enqueueSE(const Theorem &thm)
Check if the current context is inconsistent.
std::vector< std::pair< std::string, Expr > > d_boundVarStack
Bound variable stack: a vector of pairs
Expr parseExpr(const Expr &e)
Parse the generic expression.
virtual bool check(const Expr &e)=0
Check the validity of e in the current context.
#define DebugAssert(cond, str)
bool isType() const
Expr represents a type.
bool inconsistent()
Check if the current context is inconsistent.
Expr newClosureExpr(int kind, const Expr &var, const Expr &body)
void registerKinds(Theory *theory, std::vector< int > &kinds)
Register new kinds with the given theory.
void setRep(const Theorem &e) const
void setSig(const Theorem &e) const
void registerTheory(Theory *theory, std::vector< int > &kinds, bool hasSolver=false)
Register a new theory.
std::vector< Theory * > d_theories
Array of registered theories.
virtual Theorem rewriteIteFalse(const Expr &e)=0
==> ITE(FALSE, e1, e2) == e2
virtual ~Theory(void)
Destructor.
Expr newBoundVarExpr(const std::string &name, const std::string &uid)
Theorem renameExpr(const Expr &e)
Derived rule to create a new name for an expression.
const Expr & getExpr() const
virtual void assignValue(const Expr &t, const Expr &val)
Assigns t a concrete value val. Used in model generation.
std::map< std::string, Expr > d_globals
Database of declared identifiers.
Theorem getModelValue(const Expr &e)
Enqueue a fact to be sent to the SearchEngine.
const std::string & getKindName(int kind)
Return the name associated with a kind. The kind must already be registered.
std::hash_map< int, Theory * > d_theoryMap
Array mapping kinds to theories.
Type lookupTypeExpr(const std::string &name)
Lookup type by name. Return Null if no such type exists.
Op newFunction(const std::string &name, const Type &type, bool computeTransClosure)
Create a new uninterpreted function.
void addGlobalLemma(const Theorem &thm, int priority=0)
Add a global lemma.
void assignValue(const Expr &t, const Expr &val)
Assign t a concrete value val. Used in model generation.
Theorem simplify(const Expr &e)
Top-level simplifier.
virtual void addSplitter(const Expr &e, int priority)=0
Suggest a splitter to the Sat engine.
virtual Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
virtual Theorem substitutivityRule(const Expr &e, const Theorem &thm)=0
Optimized case for expr with one child.
std::string toString() const
ExprMap< Expr > * d_parseCache
Current cache being used for parser.
Theorem rewriteCC(const Expr &e)
Rewrite a term w.r.t. congruence closure (must be setup with setupCC())
std::string toString() const
Print the expression to a string.
Expr newVar(const std::string &name, const Type &type)
Create a new variable given its name and type.
void unregisterKinds(Theory *theory, std::vector< int > &kinds)
Unregister kinds for a theory.
int getOpKind() const
Get kind of operator (for APPLY Exprs only)
const Theorem & getSig() const
virtual Theorem rewriteIteSame(const Expr &e)=0
==> ITE(c, e, e) == e
const Theorem & getRep() const
CoreSatAPI * d_coreSatAPI
const Expr & getBody() const
Get the body of the closure Expr.
std::string int2string(int n)
Expr simplifyExpr(const Expr &e)
Simplify a term e w.r.t. the current context.
const Expr & getRHS() const
const std::string & getName() const
Get the name of the theory (for debugging purposes)
const Theorem & findRef(const Expr &e)
Return the find as a reference: expr must have a find.
Theorem getModelValue(const Expr &e)
Fetch the concrete assignment to the variable during model generation.
Type newTypeExpr(const std::string &name)
Create a new uninterpreted type with the given name.
Expr getTypePred(const Type &t, const Expr &e)
Calls the correct theory to compute a type predicate.
std::string toString() const
const Expr & trueExpr()
Return TRUE Expr.
Expr addBoundVar(const std::string &name, const Type &type)
Create and add a new bound variable to the stack, for parseExprOp().
virtual Type computeBaseType(const Type &tp)
Compute the base type of the top-level operator of an arbitrary type.
std::hash_map< std::string, Expr > d_boundVarMap
Map for bound vars.
virtual Theorem rewriteIteTrue(const Expr &e)=0
==> ITE(TRUE, e1, e2) == e1
void installID(const std::string &name, const Expr &e)
Install name as a new identifier associated with Expr e.
ExprManager * getEM()
Access to ExprManager.
void registerAtom(const Expr &e, const Theorem &thm)
Register an atomic formula of interest.
void getModelTerm(const Expr &e, std::vector< Expr > &v)
Calls the correct theory to get all of the terms that need to be assigned values in the concrete mode...
void setInconsistent(const Theorem &e)
Theorem updateHelper(const Expr &e)
Update the children of the term e.
Op lookupFunction(const std::string &name, Type *type)
Look up a function by name.
void setType(const Type &t) const
Set the cached type.
Type getBaseType(const Expr &e)
Compute (or look up in cache) the base type of e and return the result.
void updateCC(const Theorem &e, const Expr &d)
Update a term w.r.t. congruence closure (must be setup with setupCC())
virtual Theorem simplifyOp(const Expr &e)
Recursive simplification step.
bool findReduced(const Expr &e)
Return true iff e is find-reduced.
Theorem findReduce(const Expr &e)
Return find-reduced version of e.
int getNumTheories()
Return the number of registered theories.
virtual bool inconsistent()
Check if the current context is inconsistent.
virtual void computeModelTerm(const Expr &e, std::vector< Expr > &v)
Add variables from 'e' to 'v' for constructing a concrete model.
bool isAbsLiteral() const
Test if e is an abstract literal.
Theorem typePred(const Expr &e)
Return a theorem for the type predicate of e.
const std::vector< Expr > & getVars() const
Get bound variables from a closure Expr.
void assertEqualities(const Theorem &e)
Assert a system of equations (1 or more).
Op mkOp() const
Make the expr into an operator.
const Expr & getLHS() const
Expr newVarExpr(const std::string &s)
ExprMap< Expr > d_parseCacheTop
Top-level cache for parser.
Expr getTCC(const Expr &e)
Compute the TCC of e, or the subtyping predicate, if e is a type.
virtual void registerAtom(const Expr &e, const Theorem &thm)
Theorem rewriteIte(const Expr &e)
Derived rule for rewriting ITE.
void invalidateSimpCache()
Invalidate the simplifier's cache tag.
Theorem reflexivityRule(const Expr &a)
==> a == a
CommonProofRules * d_commonRules
Commonly used proof rules.
Expr lookupVar(const std::string &name, Type *type)
Lookup variable and return it and its type. Return NULL Expr if it doesn't exist yet.
Theory * theoryOf(int kind)
Return the theory associated with a kind.
Type getType() const
Get the type. Recursively compute if necessary.
Expr andExpr(const std::vector< Expr > &children)
Theorem find(const Expr &e)
Return the theorem that e is equal to its find.
virtual Theorem varIntroSkolem(const Expr &e)=0
Retrun a theorem "|- e = v" for a new Skolem constant v.
ExprMap< Expr > d_parseCacheOther
Alternative cache for parser when not at top-level.
Theory(void)
Private default constructor.
Theorem transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)
(a1 == a2) & (a2 == a3) ==> (a1 == a3)
Theorem symmetryRule(const Theorem &a1_eq_a2)
a1 == a2 ==> a2 == a1
iterator end() const
End iterator.