43 d_processQueue(core->getCM()->getCurrentContext()),
44 d_processQueueKind(core->getCM()->getCurrentContext()),
45 d_processIndex(core->getCM()->getCurrentContext(), 0),
46 d_typeComplete(core->getCM()->getCurrentContext(), false)
53 "datatype: instantiate: Expected find(e)=e");
56 "datatype: instantiate: Expected single label in u");
59 +
"\n\n for expression: "+e.
toString());
62 for (; c_it != c_end; ++c_it) {
63 if ((u & ((
Unsigned)1 <<
unsigned((*c_it).second))) != 0)
break;
66 "datatype: instantiate: couldn't find constructor");
67 Expr cons = (*c_it).first;
72 if (consType.
arity() == 1) {
79 for (
int i = 0; i < consType.
arity()-1; ++i) {
80 vars.push_back(
getEM()->newBoundVarExpr(consType[i]));
93 "datatype: initializeLabels: Expected find(e)=e");
98 "datatype: initializeLabels: expected unlabeled expr");
102 "datatype: initializeLabels: Couldn't find constructor "
104 unsigned position = c[cons];
127 "datatype: mergeLabels: Expected hasFind(e2)");
129 const Expr& f = fthm.getRHS();
132 "mergeLabels: expr is not labeled");
137 if (e2 != f)
d_facts.push_back(fthm);
145 if (uNew != 0 && ((uNew - 1) & uNew) == 0) {
152 unsigned position,
bool positive)
155 "datatype: mergeLabels2: Expected hasFind(e)");
157 const Expr& f = fthm.getRHS();
159 "mergeLabels2: expr is not labeled");
164 if (u == uNew)
return;
165 }
else if ((u & uNew) != 0) uNew = u - uNew;
167 if (e != f)
d_facts.push_back(fthm);
172 else if (((uNew - 1) & uNew) == 0) {
185 "checkSat: expr is not labeled");
187 if ((u & (u-1)) != 0) {
190 "splitter should have been resolved");
195 +
"\n\n for expression: "+e.
toString());
198 for (; c_it != c_end; ++c_it) {
199 if ((u & ((
Unsigned)1 <<
unsigned((*c_it).second))) != 0)
break;
202 "datatype: checkSat: couldn't find constructor");
289 if (sigNew == dsig)
return;
303 if (!repEQsigNew.
isNull()) {
309 int k, ar(d.
arity());
310 for (k = 0; k < ar; ++k) {
311 if (sigNew[k] != dsig[k]) {
bool isConstructor(const Expr &e)
TheoryCore * theoryCore()
Get a pointer to theoryCore.
CDMap< Expr, SmartCDO< Unsigned > > d_labels
Data structure of expressions in CVC3.
void addSplitter(const Expr &e, int priority=0)
Suggest a splitter to the SearchEngine.
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
An exception thrown by the parser.
Expr datatypeTestExpr(const std::string &constructor, const Expr &arg)
virtual void setInconsistent(const Theorem &e)
Make the context inconsistent; The formula proved by e must FALSE.
void setupCC(const Expr &e)
Setup a term for congruence closure (must have sig and rep attributes)
CDList< Expr > d_splitters
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.
Expr getConstructor(const Expr &e)
DatatypeProofRules * d_rules
MS C++ specific settings.
virtual void enqueueFact(const Theorem &e)
Submit a derived fact to the core from a decision procedure.
bool isTranslated() const
Expr eqExpr(const Expr &right) const
bool isSelector(const Expr &e)
#define DebugAssert(cond, str)
ExprMap< ExprMap< unsigned > > d_datatypes
Expr newClosureExpr(int kind, const Expr &var, const Expr &body)
void setRep(const Theorem &e) const
void setSig(const Theorem &e) const
bool canCollapse(const Expr &e)
Abstract interface for recursive datatype proof rules.
T & push_back(const T &data, int scope=-1)
Expr getOpExpr() const
Get expression of operator (for APPLY Exprs only)
const Expr & getExpr() const
CDO< bool > d_typeComplete
CDO< unsigned > d_splittersIndex
This theory handles datatypes.
std::string toString() const
Print the expression to a string.
const Theorem & getSig() const
const Theorem & getRep() const
virtual Theorem rewriteSelCons(const CDList< Theorem > &facts, const Expr &e)=0
const Expr & getRHS() const
Expr findExpr(const Expr &e)
Return the find of e, or e if it has no find.
CDO< unsigned > d_processIndex
std::string toString() const
const Expr & falseExpr()
Return FALSE Expr.
virtual Theorem decompose(const Theorem &e)=0
void initializeLabels(const Expr &e, const Type &t)
ExprManager * getEM()
Access to ExprManager.
void mergeLabels(const Theorem &thm, const Expr &e1, const Expr &e2)
virtual Theorem noCycle(const Expr &e)=0
void setTranslated(int scope=-1) const
Set the translated flag for this Expr.
bool isTester(const Expr &e)
CDList< Theorem > d_facts
Theorem updateHelper(const Expr &e)
Update the children of the term e.
virtual Theorem dummyTheorem(const CDList< Theorem > &facts, const Expr &e)=0
void checkSat(bool fullEffort)
Check for satisfiability in the theory.
void setSelected() const
Set the Selected flag for this Expr.
CDO< bool > d_splitterAsserted
void update(const Theorem &e, const Expr &d)
Notify a theory of a new equality.
void instantiate(const Expr &e, const Unsigned &u)
An exception to be thrown by the smtlib translator.
virtual Theorem rewriteTestCons(const Expr &e)=0
Op mkOp() const
Make the expr into an operator.
const Expr & getLHS() const
void invalidateSimpCache()
Invalidate the simplifier's cache tag.
Theorem reflexivityRule(const Expr &a)
==> a == a
void setup(const Expr &e)
Set up the term e for call-backs when e or its children change.
Type getType() const
Get the type. Recursively compute if necessary.
CDList< ProcessKinds > d_processQueueKind
CDList< Theorem > d_processQueue
Theorem find(const Expr &e)
Return the theorem that e is equal to its find.
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