42 :
Theory(core,
"Datatypes"),
43 d_labels(core->getCM()->getCurrentContext()),
44 d_facts(core->getCM()->getCurrentContext()),
45 d_splitters(core->getCM()->getCurrentContext()),
46 d_splittersIndex(core->getCM()->getCurrentContext(), 0),
47 d_splitterAsserted(core->getCM()->getCurrentContext(), false),
48 d_smartSplits(core->getFlags()[
"dt-smartsplits"].getBool())
78 "datatype: instantiate: Expected find(e)=e");
81 "datatype: instantiate: Expected single label in u");
84 +
"\n\n for expression: "+e.
toString());
87 for (; c_it != c_end; ++c_it) {
88 if ((u & (
Unsigned(1) << (
unsigned)(*c_it).second)) != 0)
break;
91 "datatype: instantiate: couldn't find constructor");
92 const Expr& cons = (*c_it).first;
97 if (consType.
arity() == 1) {
103 for (
int i = 0; i < consType.
arity()-1; ++i) {
104 vars.push_back(
getEM()->newBoundVarExpr(consType[i]));
115 "datatype: initializeLabels: Expected find(e)=e");
120 "datatype: initializeLabels: expected unlabeled expr");
124 "datatype: initializeLabels: Couldn't find constructor "
148 "datatype: mergeLabels: Expected find(e2)=e2");
151 "mergeLabels: expr is not labeled");
161 if (uNew != 0 && ((uNew - 1) & uNew) == 0) {
168 unsigned position,
bool positive)
171 "datatype: mergeLabels2: Expected find(e)=e");
173 "mergeLabels2: expr is not labeled");
178 if (u == uNew)
return;
179 }
else if ((u & uNew) != 0) uNew = u - uNew;
185 else if (((uNew - 1) & uNew) == 0) {
210 else if (expr.
isNot()) {
211 if (expr[0].getOpKind() ==
TESTER) {
216 else if (expr[0].isEq() &&
232 for (; c_it != c_end; ++c_it) {
233 if ((u1 & u2 & ((
Unsigned)1 <<
unsigned((*c_it).second))) != 0) {
236 for (
unsigned i = 0; i < selectors.size(); ++i) {
237 Expr e1 =
Expr(selectors[i].mkOp(), expr[0][0]);
239 if (conj.
isNull()) conj = e2;
245 conj = (e1 && e2).impExpr(!conj);
246 if (bigConj.
isNull()) bigConj = conj;
247 else bigConj = bigConj.
andExpr(conj);
268 "checkSat: expr is not labeled");
270 if ((u & (u-1)) != 0) {
273 "splitter should have been resolved");
278 +
"\n\n for expression: "+e.
toString());
282 for (; c_it != c_end; ++c_it) {
283 if ((u & ((
Unsigned)1 <<
unsigned((*c_it).second))) != 0) {
287 DebugAssert(vec.size() > 1,
"datatype: checkSat: expected 2 or more possible constructors");
296 "checkSat: expr is not labeled");
298 if ((u & (u-1)) != 0) {
300 unsigned pos =
getConsPos(selectorInfo.first);
301 if ((u & ((
Unsigned)1 << pos)) != 0) {
304 "splitter should have been resolved");
372 "Expected datatype");
392 if (sigNew == dsig)
return;
404 if (!repEQsigNew.
isNull()) {
409 int k, ar(d.
arity());
410 for (k = 0; k < ar; ++k) {
411 if (sigNew[k] != dsig[k]) {
451 FatalAssert(
false,
"Unexpected kind in TheoryDatatype::checkType"
458 bool enumerate,
bool computeSize)
461 "Unexpected kind in TheoryDatatype::finiteTypeInfo");
471 bool getSize = enumerate || computeSize;
472 Unsigned totalSize = 0, thisSize, size;
473 vector<Unsigned> sizes;
478 for (; c_it != c_end; ++c_it) {
479 const Expr& cons = (*c_it).first;
482 for (j = 0; j < funType.
arity()-1; ++j) {
483 Expr e2 = funType[j];
495 thisSize = thisSize * size;
497 if (thisSize > 1000000) thisSize = 0;
506 sizes.push_back(thisSize);
507 totalSize = totalSize + thisSize;
516 for (; i < sizes.size(); ++i, ++c_it) {
520 else n = n - sizes[i];
522 if (i == sizes.size() && n != 0) {
526 const Expr& cons = (*c_it).first;
528 if (funType.
arity() == 1) {
532 vector<Expr> kids(funType.
arity()-1);
535 for (
int j = funType.
arity()-2; j >= 0; --j) {
570 Type t = op.lookupType();
584 for (; i != iend; ++i, ++j) {
588 +
"\n\nhas the following type:\n\n "
589 + (*i).getType().getExpr().toString()
590 +
"\n\nbut the expected type is:\n\n "
592 +
"\n\nin datatype function application:\n\n "
601 DebugAssert(
false,
"Unexpected kind in datatype::computeType: "
622 if (op.getKind() !=
SELECTOR)
return tcc;
644 os <<
"DATATYPE" <<
endl;
647 if (first) first =
false;
648 else os <<
"," <<
endl;
651 "Unknown datatype: "+(*i).toString());
654 bool firstCons(
true);
655 for (; c_it != c_end; ++c_it) {
659 else firstCons =
false;
660 const Expr& cons = (*c_it).first;
664 for (
unsigned j = 0; j < sels.size(); ++j) {
671 os << sels[j] <<
space <<
": ";
672 os << sels[j].getType().getExpr()[1];
696 if(first) first =
false;
697 else os <<
"," <<
space;
710 DebugAssert(
false,
"TheoryDatatype::print: Unexpected kind: "
738 "TheoryDatatype::parseExprOp:\n e = "+e.
toString());
741 "Expected ID kind for first elem in list expr");
743 const Expr& c1 = e[0][0];
748 "Empty DATATYPE expression\n"
749 " (expected at least one datatype): "+e.
toString());
753 vector<Expr> allConstructorNames;
754 vector<Expr> constructorNames;
756 vector<Expr> allSelectorNames;
757 vector<Expr> selectorNames;
758 vector<Expr> selectorNamesKids;
760 vector<Expr> allTypes;
762 vector<Expr> typesKids;
765 Expr dt, constructor, selectors, selector;
769 for (i = 0; i < e.
arity()-1; ++i) {
772 "Bad formed datatype expression"
775 "Expected ID kind for datatype name"
777 names.push_back(dt[0][0]);
778 if (namesMap.
count(dt[0][0]) != 0) {
779 throw ParserException(
"Datatype name used more than once"+dt[0][0].getString());
781 namesMap.
insert(dt[0][0],
true);
785 for (i = 0; i < e.
arity()-1; ++i) {
788 "Expected non-empty list for datatype constructors"
793 for(j = 0; j < dt.arity(); ++j) {
796 (constructor.
arity() == 1 || constructor.
arity() == 2),
797 "Unexpected constructor"+constructor.
toString());
799 "Expected ID kind for constructor name"
801 constructorNames.push_back(constructor[0][0]);
803 if (constructor.
arity() == 2) {
804 selectors = constructor[1];
806 "Non-empty list expected as second argument of constructor:\n"
810 for (k = 0; k < selectors.
arity(); ++k) {
811 selector = selectors[k];
813 "Expected list of arity 2 for selector"
816 "Expected ID kind for selector name"
818 selectorNamesKids.push_back(selector[0][0]);
819 if (selector[1].getKind() ==
ID && namesMap.
count(selector[1][0]) > 0) {
820 typesKids.push_back(selector[1][0]);
823 typesKids.push_back(
parseExpr(selector[1]));
826 selectorNames.push_back(
Expr(
RAW_LIST, selectorNamesKids));
827 selectorNamesKids.clear();
836 allConstructorNames.push_back(
Expr(
RAW_LIST, constructorNames));
837 constructorNames.clear();
838 allSelectorNames.push_back(
Expr(
RAW_LIST, selectorNames));
839 selectorNames.clear();
860 const vector<string>& constructors,
861 const vector<vector<string> >& selectors,
862 const vector<vector<Expr> >& types)
864 vector<string> names;
865 vector<vector<string> > constructors2;
866 vector<vector<vector<string> > > selectors2;
867 vector<vector<vector<Expr> > > types2;
868 names.push_back(name);
869 constructors2.push_back(constructors);
870 selectors2.push_back(selectors);
871 types2.push_back(types);
872 return dataType(names, constructors2, selectors2, types2);
879 const vector<vector<string> >& allConstructors,
880 const vector<vector<vector<string> > >& allSelectors,
881 const vector<vector<vector<Expr> > >& allTypes)
883 vector<Expr> returnTypes;
886 bool thisWellFounded;
888 if (names.size() != allConstructors.size() ||
889 allConstructors.size() != allSelectors.size() ||
890 allSelectors.size() != allTypes.size()) {
892 (
"dataType: vector sizes don't match");
899 vector<Type> funTypeArgs;
908 for (i = 0; i < names.size(); ++i) {
912 (
"Attempt to define datatype "+names[i]+
":\n "
913 "This variable is already defined.");
917 returnTypes.push_back(e);
921 vector<Expr> selectorVec;
923 for (i = 0; i < names.size(); ++i) {
925 const vector<string>& constructors = allConstructors[i];
926 const vector<vector<string> >& selectors = allSelectors[i];
927 const vector<vector<Expr> >& types = allTypes[i];
929 if (constructors.size() == 0) {
931 (
"datatype: "+names[i]+
": must have at least one constructor");
933 if (constructors.size() != selectors.size() ||
934 selectors.size() != types.size()) {
936 (
"dataType: vector sizes at index "+
int2string(i)+
" don't match");
941 for (j = 0; j < constructors.size(); ++j) {
945 (
"Attempt to define datatype constructor "+constructors[j]+
":\n "
946 "This variable is already defined.");
950 if (selectors[j].size() != types[j].size()) {
953 ": number of selectors does not match number of types");
955 thisWellFounded =
true;
956 const vector<string>& sels = selectors[j];
957 const vector<Expr>& tps = types[j];
959 vector<Type> selTypes;
962 for (k = 0; k < sels.size(); ++k) {
966 (
"Attempt to define datatype selector "+sels[k]+
":\n "
967 "This variable is already defined.");
970 if (tps[k].isString()) {
974 (
"Unable to resolve type identifier: "+tps[k].getString());
976 }
else t =
Type(tps[k]);
979 (
"Cannot have BOOLEAN inside of datatype");
983 (
"Cannot have function inside of datatype");
986 selTypes.push_back(
Type(t));
989 thisWellFounded =
false;
993 selectorVec.push_back(s);
996 if (selTypes.size() == 0) {
1004 selectorVec.clear();
1006 string testerString =
"is_"+constructors[j];
1010 (
"Attempt to define datatype tester "+testerString+
":\n "
1011 "This variable is already defined.");
1022 bool changed, thisFinite;
1023 int firstNotWellFounded;
1026 firstNotWellFounded = -1;
1027 for (i = 0; i < names.size(); ++i) {
1030 thisWellFounded =
false;
1032 for (; c_it != c_end; ++c_it) {
1033 const Expr& cons = (*c_it).first;
1037 for (j = 0; j < funType.
arity()-1; ++j) {
1041 if (j == funType.
arity()-1) {
1045 else thisFinite =
false;
1048 thisWellFounded =
true;
1051 for (j = 0; j < funType.
arity()-1; ++j) {
1055 if (j == funType.
arity()-1) {
1058 thisWellFounded =
true;
1061 if (!thisWellFounded) {
1062 if (firstNotWellFounded == -1) firstNotWellFounded = i;
1065 if (!returnTypes[i].isWellFounded()) {
1067 returnTypes[i].setWellFounded();
1070 if (thisFinite && !returnTypes[i].isFinite()) {
1072 returnTypes[i].setFinite();
1077 if (firstNotWellFounded >= 0) {
1080 (
"Datatype "+names[firstNotWellFounded]+
" has no finite terms");
1087 const vector<Expr>& args)
1091 throw Exception(
"datatype: unknown constructor: "+constructor);
1094 "\nwhich is not a constructor");
1095 if (args.size() == 0)
return e;
1104 throw Exception(
"datatype: unknown selector: "+selector);
1107 "\nwhich is not a selector");
1116 throw Exception(
"datatype: unknown tester: is_"+constructor);
1119 "\nwhich is not a tester");
1129 "Unknown selector: "+e.
toString());
1137 "getConsForTester called on non-tester"
1148 "getConsPos called on non-constructor");
1150 if (t.isFunction()) t = t[t.arity()-1];
1153 "Could not find datatype: "+t.toString());
1156 "Could not find constructor: "+e.
toString());
1168 "TheoryDatatype::getconstant: too deep recursion depth");
1175 for (; i != iend; ++i) {
1176 const Expr& cons = (*i).first;
1178 d_getConstantStack.erase(t.
getExpr());
1182 for (i = c.
begin(), iend = c.end(); i != iend; ++i) {
1183 const Expr& cons = (*i).first;
1187 for (; j < funType.
arity()-1; ++j) {
1191 DebugAssert(!args.back().isNull(),
"Expected non-null");
1193 if (j == funType.
arity()-1) {
1194 d_getConstantStack.erase(t.
getExpr());
1198 for (i = c.
begin(), iend = c.end(); i != iend; ++i) {
1199 const Expr& cons = (*i).first;
1203 for (; j < funType.
arity()-1; ++j) {
1205 if (t_j == t)
break;
1207 if (args.back().isNull())
break;
1209 if (j == funType.
arity()-1) {
1210 d_getConstantStack.erase(t.
getExpr());
1218 "Expected non-bool, non-function type");
1222 d_getConstantStack.erase(t.
getExpr());
1232 "Couldn't find reachable predicate");
1244 "canCollapse: Expected find(e[0])=e[0]");
1248 if ((u & uCons) == 0)
return true;
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.
ExprStream & pop(ExprStream &os)
Restore the indentation.
void addSharedTerm(const Expr &e)
Notify theory of a new shared term.
bool isConstructor(const Expr &e)
const Expr & getExpr() const
iterator begin() const
Begin iterator.
ExprStream & printAST(ExprStream &os) const
Print the top node and then recurse through the children */.
TheoryCore * theoryCore()
Get a pointer to theoryCore.
bool isDatatype(const Type &t)
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.
static Type funType(const std::vector< Type > &typeDom, const Type &typeRan)
void setupCC(const Expr &e)
Setup a term for congruence closure (must have sig and rep attributes)
void checkType(const Expr &e)
Check that e is a valid Type expr.
const bool & d_smartSplits
CDList< Expr > d_splitters
void insert(const Expr &e, const Data &d)
virtual void mergeLabels(const Theorem &thm, const Expr &e1, const Expr &e2)
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)
virtual void update(const Theorem &e, const Expr &d)
Notify a theory of a new equality.
Expr getConstructor(const Expr &e)
Expr newSymbolExpr(const std::string &s, int kind)
void assertFact(const Theorem &e)
Assert a new fact to the decision procedure.
Expr resolveID(const std::string &name)
Resolve an identifier, for use in parseExprOp()
DatatypeProofRules * d_rules
MS C++ specific settings.
virtual void enqueueFact(const Theorem &e)
Submit a derived fact to the core from a decision procedure.
Expr getConstant(const Type &t)
Lisp-like format for automatically generated specs.
Expr eqExpr(const Expr &right) const
bool isSelector(const Expr &e)
void computeModelTerm(const Expr &e, std::vector< Expr > &v)
Add variables from 'e' to 'v' for constructing a concrete model.
virtual Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Compute information related to finiteness of types.
ExprStream & space(ExprStream &os)
Insert a single white space separator.
#define DebugAssert(cond, str)
ExprMap< ExprMap< unsigned > > d_datatypes
bool isTerm() const
Test if e is a term (as opposed to a predicate/formula)
Expr newClosureExpr(int kind, const Expr &var, const Expr &body)
void setRep(const Theorem &e) const
virtual void setup(const Expr &e)
Set up the term e for call-backs when e or its children change.
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 andExpr(const Expr &right) const
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
unsigned getConsPos(const Expr &e)
Expr getConsForTester(const Expr &e)
void registerTheory(Theory *theory, std::vector< int > &kinds, bool hasSolver=false)
Register a new theory.
Expr getOpExpr() const
Get expression of operator (for APPLY Exprs only)
Expr impExpr(const Expr &right) const
bool isWellFounded() const
void computeType(const Expr &e)
Compute and store the type of e.
const Op & getReachablePredicate(const Type &t)
Op getOp() const
Get operator from expression.
const Expr & getExpr() const
size_t count(const Expr &e) const
Op newFunction(const std::string &name, const Type &type, bool computeTransClosure)
Create a new uninterpreted function.
virtual void initializeLabels(const Expr &e, const Type &t)
CDO< unsigned > d_splittersIndex
Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Compute information related to finiteness of types.
virtual Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
Identifier is (ID (STRING_EXPR "name"))
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
Unsigned typeSizeFinite() const
Return size of a finite type; returns 0 if size cannot be determined.
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.
int getOpKind() const
Get kind of operator (for APPLY Exprs only)
const Theorem & getSig() const
Expr typeEnumerateFinite(Unsigned n) const
Return nth (starting with 0) element in a finite type.
Expr parseExprOp(const Expr &e)
Theory-specific parsing implemented by the DP.
const Theorem & getRep() const
ExprMap< Expr > d_testerMap
void newKind(int kind, const std::string &name, bool isType=false)
Register a new kind.
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
std::string int2string(int n)
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.
std::string toString() const
const Expr & falseExpr()
Return FALSE Expr.
const Expr & trueExpr()
Return TRUE Expr.
virtual Theorem decompose(const Theorem &e)=0
const std::pair< Expr, unsigned > & getSelectorInfo(const Expr &e)
void installID(const std::string &name, const Expr &e)
Install name as a new identifier associated with Expr e.
virtual void instantiate(const Expr &e, const Unsigned &u)
static Type anyType(ExprManager *em)
ExprManager * getEM()
Access to ExprManager.
virtual Theorem noCycle(const Expr &e)=0
const std::string & getName() const
bool isTester(const Expr &e)
CDList< Theorem > d_facts
Expr datatypeSelExpr(const std::string &selector, const Expr &arg)
Theorem updateHelper(const Expr &e)
Update the children of the term e.
virtual Theorem dummyTheorem(const CDList< Theorem > &facts, const Expr &e)=0
Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
void setType(const Type &t) const
Set the cached type.
void setSelected() const
Set the Selected flag for this Expr.
Type getBaseType(const Expr &e)
Compute (or look up in cache) the base type of e and return the result.
CDO< bool > d_splitterAsserted
Type boolType()
Return BOOLEAN type.
int getKind(const std::string &name)
Return a kind associated with a name. Returns NULL_KIND if not found.
Theorem solve(const Theorem &e)
An optional solver.
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
Expr datatypeConsExpr(const std::string &constructor, const std::vector< Expr > &args)
void invalidateSimpCache()
Invalidate the simplifier's cache tag.
void setWellFounded() const
Theorem reflexivityRule(const Expr &a)
==> a == a
Cardinality
Enum for cardinality of types.
ExprStream & print(ExprStream &os, const Expr &e)
Theory-specific pretty-printing.
const std::string & getString() const
DatatypeProofRules * createProofRules()
Theory * theoryOf(int kind)
Return the theory associated with a kind.
Type getType() const
Get the type. Recursively compute if necessary.
ExprMap< std::pair< Expr, unsigned > > d_selectorMap
InputLanguage lang() const
Get the current output language.
virtual ~TheoryDatatype()
ExprMap< std::vector< Expr > > d_constructorMap
virtual void checkSat(bool fullEffort)
Check for satisfiability in the theory.
ExprMap< bool > d_getConstantStack
Expr dataType(const std::string &name, const std::vector< std::string > &constructors, const std::vector< std::vector< std::string > > &selectors, const std::vector< std::vector< Expr > > &types)
void erase(const Expr &e)
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
Nice SAL-like language for manually written specs.
ExprStream & push(ExprStream &os)
Set the indentation to the current position.
iterator end() const
End iterator.
Theorem rewrite(const Expr &e)
Theory-specific rewrite rules.