43 :
Theory(core,
"Uninterpreted Functions"),
44 d_applicationsInModel(core->getFlags()[
"applications"].getBool()),
45 d_funApplications(core->getCM()->getCurrentContext()),
46 d_funApplicationsIdx(core->getCM()->getCurrentContext(), 0),
47 d_sharedIdx1(core->getCM()->getCurrentContext(), 0),
48 d_sharedIdx2(core->getCM()->getCurrentContext(), 0),
49 d_sharedTermsMap(core->getCM()->getCurrentContext())
62 kinds.push_back(
ARROW);
64 kinds.push_back(
UFUNC);
93 DebugAssert(!rel.isNull(),
"Expected known identifier");
95 "Unexpected use of transitive closure: "+expr.
toString());
105 pTable = (*i).second;
115 pList = (*i2).second;
125 pList = (*i2).second;
133 pList = (*i2).second;
135 for (l = 0; l < s; ++l) {
142 pList = (*i2).second;
144 for (l = 0; l < s; ++l) {
159 bool enqueued =
false;
164 IF_DEBUG(debugger.counter(
"Expanded lambdas (checkSat)")++;)
171 if (!fullEffort || enqueued)
return;
180 for( ; d_sharedIdx2 <
d_sharedIdx1; d_sharedIdx2 = d_sharedIdx2 + 1 ) {
185 if( f1 != f2 &&
find(f1).getRHS() !=
find(f2).getRHS() && f1_fun == f2_fun ) {
186 for(
int k = 0; k < f1.
arity(); ++k ) {
194 if( !
simplify(eq).getRHS().isBoolConst() ) {
221 IF_DEBUG(debugger.counter(
"Expanded lambdas")++;)
252 TRACE(
"model",
"TheoryUF: add function application ", e,
"");
297 if (sigNew == dsig) {
303 if (!repEQsigNew.
isNull()) {
312 int k, ar(d.
arity());
313 for (k = 0; k < ar; ++k) {
314 if (sigNew[k] != dsig[k]) {
342 (
"Function type needs at least two arguments"
345 for (; i != iend; ) {
348 if (i == iend && t.
isBool())
break;
350 (
"Function argument types must be non-Boolean: "
353 (
"Function domain or range types cannot be functions: "
362 DebugAssert(
false,
"Unexpected kind in TheoryUF::checkType"
369 bool enumerate,
bool computeSize)
378 bool getSize = enumerate || computeSize;
379 for (; i != iend; ) {
391 thisSize = thisSize * size;
393 if (thisSize > 1000000) thisSize = 0;
422 const vector<Expr>& vars = e.
getVars();
424 "TheorySimulate::computeType("+e.
toString()+
")");
425 for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
427 args.push_back((*i).getType());
438 if (funExpr.isNull()) {
440 (
"Attempt to take transitive closure of unknown id: "
443 Type funType = funExpr.getType();
446 (
"Attempt to take transitive closure of non-function:\n\n"
447 +funExpr.toString() +
"\n\n which has type: "
450 if(funType.
arity()!=3) {
452 (
"Attempt to take transitive closure of non-binary function:\n\n"
453 +funExpr.toString() +
"\n\n which has type: "
456 if (!funType[2].isBool()) {
458 (
"Attempt to take transitive closure of function:\n\n"
459 +funExpr.toString() +
"\n\n which does not return BOOLEAN");
485 "TheoryUF::computeBaseType("+t.
toString()+
")");
494 if((*i).isApply() && (*i).getOp().getExpr() == e) {
521 if((*i).isApply() && (*i).getOp().getExpr() == e) {
523 vector<Theorem> thms;
524 vector<unsigned> changed;
525 for(
int j=0; j<(*i).arity(); ++j) {
528 thms.push_back(asst);
529 changed.push_back(j);
533 if(changed.size()>0) {
547 if(appls.
size()==0) {
553 static unsigned count(0);
555 +
" : "+tp.toString()+
")");
556 for(
int i=0, iend=tp.arity()-1; i<iend; ++i) {
562 DebugAssert(args.size()>0,
"TheoryUF::computeModel()");
564 DebugAssert(i!=iend,
"TheoryUF::computeModel(): empty appls hash");
566 Expr res((*i).second); ++i;
567 for(; i!=iend; ++i) {
571 if((*i).second == res)
continue;
576 for(
int j=0, jend=args.size(); j<jend; ++j)
577 eqs.push_back(args[j].eqExpr((*i).first[j]));
583 res = cond.
iteExpr((*i).second, res);
619 Type funType(op.getType());
620 DebugAssert(funType.isFunction() || funType.isBool(),
621 "TheoryUF::computeTCC(): funType = "
622 +funType.toString());
623 if(funType.isFunction()) {
625 "TheoryUF::computeTCC(): funType = "
626 +funType.toString()+
"\n e = "+e.
toString());
627 for(
int i=0, iend=e.
arity(); i<iend; ++i) {
631 if(funType[i] != e[i].getType())
636 while(op.getKind()==
LETDECL) op = op[1];
678 for(
int i = 0, iend = e.
arity(); i < iend; ++i )
681 os <<
space <<
":transclose";
694 DebugAssert(
false,
"TheoryUF::print: SMTLIB_LANG: Unexpected expression: "
706 os<<
"ERROR:ARROW:unsupported in Simplify\n";
709 os<<
"ERROR:LAMBDA:unsupported in Simplify\n";
713 os<<
"ERROR:TRANS_CLOSURE:unsupported in Simplify\n";
716 os<<
"ERROR:TYPEDECL:unsupported in Simplify\n";
724 if(first) first =
false;
732 DebugAssert(
false,
"TheoryUF::print: Unexpected expression: "
746 for(
int i=0, iend=e.
arity()-1; i<iend; ++i) {
747 if(first) first=
false;
752 os <<
" > " << e[e.
arity()-1];
757 os<<
"ERROR:LAMBDA:unsupported in TPTP\n";
761 os<<
"ERROR:TRANS_CLOSURE:unsupported in TPTP\n";
778 if(first) first =
false;
786 DebugAssert(
false,
"TheoryUF::print: Unexpected expression: "
804 for(
int i=0, iend=e.
arity()-1; i<iend; ++i) {
805 if(first) first=
false;
806 else os <<
"," <<
space;
809 os << push <<
")" <<
pop <<
pop;
824 const vector<Expr>& vars = e.
getVars();
827 for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
829 if(first) first =
false;
830 else os << push <<
"," <<
pop <<
space;
837 os << push <<
"): " <<
pushdag << push
847 if(first) first =
false;
848 else os <<
"," <<
space;
863 DebugAssert(
false,
"TheoryUF::print: Unexpected expression: "
873 throw SmtlibException(
"TheoryUF::print: Expected 2 or more arguments to ARROW");
878 bool oldDagFlag = os.
dagFlag(
false);
879 int iend = e.
arity();
880 if (e[iend-1].getKind() ==
BOOLEAN) --iend;
881 for(
int i=0; i<iend; ++i) {
882 if (i != 0) os <<
space;
898 throw SmtlibException(
"TheoryUF::print: Expected 2 or more arguments to ARROW");
902 bool oldDagFlag = os.
dagFlag(
false);
904 for(
int i = 0; i < e.
arity() - 1; ++i ) {
923 os <<
"(" <<
push <<
"ARROW";
924 for(
int i=0, iend=e.
arity(); i<iend; ++i)
936 else if(e[0].isString()) os << e[0].
getString();
941 os <<
"(" << push <<
"LAMBDA" <<
space;
942 const vector<Expr>& vars = e.
getVars();
945 for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
947 if(first) first =
false;
949 os <<
"(" << push << *i;
954 os << push <<
")" <<
pop <<
pop;
965 for (
int i=0, iend=e.
arity(); i<iend; ++i)
971 DebugAssert(
false,
"TheoryUF::print: Unexpected expression: "
985 for (
int i=1, iend=e.arity(); i<iend; ++i)
986 os <<
"," <<
space << e[i];
997 throw SmtlibException(
"TheoryUF::print: Unexpected expression for SPASS_LANG: "
1021 "TheoryUF::parseExprOp:\n e = "+e.
toString());
1029 for(; i!=iend; ++i) args.push_back(
parseExpr(*i));
1034 "Expected identifier");
1039 if (!
theoryCore()->getFlags()[
"old-func-syntax"].getBool()) {
1040 throw ParserException(
"You seem to be using the old syntax for function types.\n"
1041 "Please convert to the new syntax or run with +old-func-syntax");
1048 for (; i != iend; ++i) {
1052 else k.push_back(arg);
1072 "TRANS_CLOSURE expression\n"
1073 " (expected 3 arguments): "+e.
toString());
1074 const string& name = e[1][0].
getString();
1077 throw ParserException(
"Attempt to take transitive closure of unknown "
1085 vector<pair<string,Type> > vars;
1087 if(i->getKind() !=
RAW_LIST || i->arity() < 2)
1089 "expression: "+i->toString()+
1095 for(
int j=0, jend=i->arity()-1; j<jend; ++j) {
1096 if((*i)[j].getKind() !=
ID)
1098 " expression: "+(*i)[j].toString()+
1100 vars.push_back(pair<string,Type>((*i)[j][0].getString(), tp));
1104 vector<Expr> boundVars;
1105 for(vector<pair<string,Type> >::iterator i=vars.begin(), iend=vars.end();
1107 boundVars.push_back(
addBoundVar(i->first, i->second));
1121 for(; i!=iend; ++i) args.push_back(
parseExpr(*i));
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.
for output in SPASS format
const Expr & getExpr() const
iterator begin() const
Begin iterator.
Type computeBaseType(const Type &t)
Compute the base type of the top-level operator of an arbitrary type.
ExprStream & printAST(ExprStream &os) const
Print the top node and then recurse through the children */.
TheoryCore * theoryCore()
Get a pointer to theoryCore.
void setRewriteNormal() const
const std::string fixConstName(const std::string &s)
Data structure of expressions in CVC3.
Cardinality card() const
Return cardinality of type.
void addSplitter(const Expr &e, int priority=0)
Suggest a splitter to the SearchEngine.
ExprMap< CDList< Theorem > * > appearsFirstMap
ExprManager * getEM() const
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Expr iteExpr(const Expr &thenpart, const Expr &elsepart) const
An exception thrown by the parser.
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)
ExprMap< CDList< Theorem > * > appearsSecondMap
void addToNotify(Theory *i, const Expr &e) const
Add (e,i) to the notify list of this expression.
void addSharedTerm(const Expr &e)
Notify theory of a new shared term.
An exception to be thrown at typecheck error.
void setup(const Expr &e)
Set up the term e for call-backs when e or its children change.
virtual Theorem applyLambda(const Expr &e)=0
Beta reduction: |- (lambda x. f(x))(arg) = f(arg)
CDO< size_t > d_sharedIdx2
Expr resolveID(const std::string &name)
Resolve an identifier, for use in parseExprOp()
for output in TPTP format
Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
bool computeTransClosure() const
MS C++ specific settings.
virtual void enqueueFact(const Theorem &e)
Submit a derived fact to the core from a decision procedure.
virtual Theorem relToClosure(const Theorem &rel)=0
ExprStream & print(ExprStream &os, const Expr &e)
Theory-specific pretty-printing.
Lisp-like format for automatically generated specs.
Expr eqExpr(const Expr &right) const
CDMap< Expr, bool > d_sharedTermsMap
The set of all shared terms.
virtual Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Compute information related to finiteness of types.
virtual Expr parseExprOp(const Expr &e)
Theory-specific parsing implemented by the DP.
ExprStream & space(ExprStream &os)
Insert a single white space separator.
Translator * getTranslator() const
Theorem rewriteAnd(const Expr &e)
==> AND(e1,e2) IFF [simplified expr]
#define DebugAssert(cond, str)
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
void setSig(const Theorem &e) const
CDList< Expr > d_funApplications
Backtracking list of function applications.
T & push_back(const T &data, int scope=-1)
const std::vector< Expr > & getKids() const
const bool & d_applicationsInModel
Flag to include function applications to the concrete model.
CDO< size_t > d_funApplicationsIdx
Pointer to the last unprocessed element (for lambda expansions)
void registerTheory(Theory *theory, std::vector< int > &kinds, bool hasSolver=false)
Register a new theory.
ExprStream & pushdag(ExprStream &os)
Context * getCurrentContext()
Expr getOpExpr() const
Get expression of operator (for APPLY Exprs only)
Expr newBoundVarExpr(const std::string &name, const std::string &uid)
Op getOp() const
Get operator from expression.
const Expr & getExpr() const
virtual void assignValue(const Expr &t, const Expr &val)
Assigns t a concrete value val. Used in model generation.
const_iterator end() const
CommonProofRules * getCommonRules()
Get a pointer to common proof rules.
void computeType(const Expr &e)
Compute and store the type of e.
virtual Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
Identifier is (ID (STRING_EXPR "name"))
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.
void checkType(const Expr &e)
Check that e is a valid Type expr.
virtual void computeType(const Expr &e)
Compute and store the type of e.
void print(InputLanguage lang, bool dagify=true) const
Print the expression in the specified format.
int getOpKind() const
Get kind of operator (for APPLY Exprs only)
const Theorem & getSig() const
const Theorem & getRep() const
ExprMap< TCMapPair * > d_transClosureMap
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!
void computeModelTerm(const Expr &e, std::vector< Expr > &v)
Add variables from 'e' to 'v' for constructing a concrete model.
const Expr & getBody() const
Get the body of the closure Expr.
std::string int2string(int n)
const Expr & getRHS() const
Expr findExpr(const Expr &e)
Return the find of e, or e if it has no find.
Theorem getModelValue(const Expr &e)
Fetch the concrete assignment to the variable during model generation.
CDO< size_t > d_sharedIdx1
The pointers to the last unprocessed shared pair.
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().
Expr lambdaExpr(const std::vector< Expr > &vars, const Expr &body)
Create a new LAMBDA-abstraction.
Expr transClosureExpr(const std::string &name, const Expr &e1, const Expr &e2)
Create a transitive closure expression.
ExprManager * getEM()
Access to ExprManager.
ExprStream & popdag(ExprStream &os)
const std::string & getName() const
void computeModel(const Expr &e, std::vector< Expr > &vars)
Compute the value of a compound variable from the more primitive ones.
ContextManager * getCM() const
Theorem updateHelper(const Expr &e)
Update the children of the term e.
Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Compute information related to finiteness of types.
Abstract interface for uninterpreted function/predicate proof rules.
struct CVC3::TheoryUF::TCMapPair TCMapPair
UFProofRules * createProofRules()
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 assertFact(const Theorem &e)
Assert a new fact to the decision procedure.
void update(const Theorem &e, const Expr &d)
Notify a theory of a new equality.
std::string to_lower(const std::string &src)
int getKind(const std::string &name)
Return a kind associated with a name. Returns NULL_KIND if not found.
An exception to be thrown by the smtlib translator.
An exception to be thrown by the smtlib translator.
const std::vector< Expr > & getVars() const
Get bound variables from a closure Expr.
Op mkOp() const
Make the expr into an operator.
const Expr & getLHS() const
Expr getTCC(const Expr &e)
Compute the TCC of e, or the subtyping predicate, if e is a type.
const_iterator begin() const
Theorem reflexivityRule(const Expr &a)
==> a == a
Theorem substitutivityRule(const Op &op, const std::vector< Theorem > &thms)
(c_1 == d_1) & ... & (c_n == d_n) ==> op(c_1,...,c_n) == op(d_1,...,d_n)
Cardinality
Enum for cardinality of types.
const std::string & getString() const
void checkSat(bool fullEffort)
Check for satisfiability in the theory.
Theory * theoryOf(int kind)
Return the theory associated with a kind.
Type getType() const
Get the type. Recursively compute if necessary.
InputLanguage lang() const
Get the current output language.
void printSmtLibShared(ExprStream &os, const Expr &e)
virtual Theorem relTrans(const Theorem &t1, const Theorem &t2)=0
Expr andExpr(const std::vector< Expr > &children)
Theorem rewrite(const Expr &e)
Theory-specific rewrite rules.
Theorem find(const Expr &e)
Return the theorem that e is equal to its find.
for output into Simplify format
bool dagFlag(bool flag=true)
Set the DAG flag (return previous value)
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.
virtual Theorem iffTrueElim(const Theorem &e)=0
ExprStream & push(ExprStream &os)
Set the indentation to the current position.
iterator end() const
End iterator.