22 #ifndef _cvc3__expr_h_
23 #define _cvc3__expr_h_
134 friend class ExprHasher;
140 friend class ::CInterface;
151 VALID_IS_ATOMIC = 0x2,
155 REWRITE_NORMAL = 0x8,
159 WELL_FOUNDED = 0x800,
161 COMPUTE_TRANS_CLOSURE = 0x1000,
163 CONTAINS_BOUND_VAR = 0x00020000,
165 USES_CC = 0x00080000,
167 VALID_TERMINALS_CONST = 0x00100000,
169 TERMINALS_CONST = 0x00200000
176 IMPLIED_LITERAL = 0x10,
177 IS_USER_ASSUMPTION = 0x20,
178 IS_INT_ASSUMPTION = 0x40,
180 IS_TRANSLATED = 0x100,
181 IS_USER_REGISTERED_ATOM = 0x200,
182 IS_SELECTED = 0x2000,
183 IS_STORED_PREDICATE = 0x4000,
184 IS_REGISTERED_ATOM = 0x8000,
185 IN_USER_ASSUMPTION = 0x00010000,
187 NOT_ARRAY_NORMALIZED = 0x00040000
230 :
public std::iterator<std::input_iterator_tag,Expr,ptrdiff_t>
234 std::vector<Expr>::const_iterator
d_it;
238 iterator(std::vector<Expr>::const_iterator it): d_it(it) { }
247 return d_it == i.
d_it;
303 const Expr& child2,
const Expr& child3);
304 Expr(
const Op& op,
const std::vector<Expr>& children,
312 Expr notExpr()
const;
316 Expr iteExpr(
const Expr& thenpart,
const Expr& elsepart)
const;
321 Expr skolemExpr(
int i)
const;
328 Expr substExpr(
const std::vector<Expr>& oldTerms,
329 const std::vector<Expr>& newTerms)
const;
333 Expr substExprQuant(
const std::vector<Expr>& oldTerms,
334 const std::vector<Expr>& newTerms)
const;
360 bool isString()
const;
361 bool isClosure()
const;
362 bool isQuantifier()
const;
363 bool isLambda()
const;
364 bool isApply()
const;
365 bool isSymbol()
const;
366 bool isTheorem()
const;
390 bool isAtomic()
const;
396 bool isAtomicFormula()
const;
399 {
return isQuantifier() || isAtomicFormula(); }
404 {
return (isAtomicFormula() || (isNot() && (*
this)[0].isAtomicFormula())); }
407 {
return (isAbsAtomicFormula() || (isNot() && (*
this)[0].isAbsAtomicFormula())); }
409 bool isBoolConnective()
const;
411 bool isPropAtom()
const {
return !isTerm() && !isBoolConnective(); }
414 {
return (isNot() && (*
this)[0].isPropAtom()) || isPropAtom(); }
416 bool containsTermITE()
const;
419 bool isEq()
const {
return getKind() ==
EQ; }
422 bool isOr()
const {
return getKind() ==
OR; }
438 const std::string& getName()
const;
440 const std::string& getUid()
const;
443 const std::string& getString()
const;
445 const std::vector<Expr>& getVars()
const;
447 const Expr& getExistential()
const;
449 int getBoundIndex()
const;
452 const Expr& getBody()
const;
455 void setTriggers(
const std::vector<std::vector<Expr> >& triggers)
const;
456 void setTriggers(
const std::vector<Expr>& triggers)
const;
457 void setTrigger(
const Expr& trigger)
const;
458 void setMultiTrigger(
const std::vector<Expr>& multiTrigger)
const;
461 const std::vector<std::vector<Expr> >& getTriggers()
const;
464 const Rational& getRational()
const;
466 const Theorem& getTheorem()
const;
472 const std::vector<Expr>& getKids()
const;
481 bool hasLastIndex()
const;
490 Expr getOpExpr()
const;
493 int getOpKind()
const;
503 const Expr& operator[](
int i)
const;
509 iterator begin()
const;
512 iterator end()
const;
520 size_t getMMIndex()
const;
525 bool hasFind()
const;
530 const Theorem& getFind()
const;
531 int getFindLevel()
const;
532 const Theorem& getEqNext()
const;
538 Type getType()
const;
540 Type lookupType()
const;
552 bool validSimpCache()
const;
555 const Theorem& getSimpCache()
const;
558 bool isValidType()
const;
561 bool validIsAtomicFlag()
const;
564 bool validTerminalsConstFlag()
const;
567 bool getIsAtomicFlag()
const;
570 bool getTerminalsConstFlag()
const;
573 bool isRewriteNormal()
const;
576 bool isFinite()
const;
579 bool isWellFounded()
const;
582 bool computeTransClosure()
const;
585 bool containsBoundVar()
const;
591 bool notArrayNormalized()
const;
594 bool isImpliedLiteral()
const;
597 bool isUserAssumption()
const;
600 bool inUserAssumption()
const;
603 bool isIntAssumption()
const;
606 bool isJustified()
const;
609 bool isTranslated()
const;
612 bool isUserRegisteredAtom()
const;
615 bool isRegisteredAtom()
const;
618 bool isSelected()
const;
621 bool isStoredPredicate()
const;
624 bool getFlag()
const;
626 void setFlag()
const;
628 void clearFlags()
const;
633 std::string toString()
const;
642 void printnodag()
const;
647 void pprintnodag()
const;
663 Expr& indent(
int n,
bool permanent =
false);
672 void setFind(
const Theorem& e)
const;
675 void setEqNext(
const Theorem& e)
const;
678 void addToNotify(
Theory* i,
const Expr& e)
const;
681 void setType(
const Type& t)
const;
684 void setSimpCache(
const Theorem& e)
const;
687 void setValidType()
const;
690 void setIsAtomicFlag(
bool value)
const;
693 void setTerminalsConstFlag(
bool value)
const;
696 void setRewriteNormal()
const;
697 void clearRewriteNormal()
const;
700 void setFinite()
const;
703 void setWellFounded()
const;
706 void setComputeTransClosure()
const;
709 void setContainsBoundVar()
const;
712 void setUsesCC()
const;
715 void setNotArrayNormalized()
const;
718 void setImpliedLiteral()
const;
721 void setUserAssumption(
int scope = -1)
const;
724 void setInUserAssumption(
int scope = -1)
const;
727 void setIntAssumption()
const;
730 void setJustified()
const;
733 void setTranslated(
int scope = -1)
const;
736 void setUserRegisteredAtom()
const;
739 void setRegisteredAtom()
const;
742 void setSelected()
const;
745 void setStoredPredicate()
const;
748 bool subExprOf(
const Expr& e)
const;
770 void setSig(
const Theorem& e)
const;
771 void setRep(
const Theorem& e)
const;
814 if(&e ==
this)
return *
this;
816 if(tmp ==
d_expr)
return *
this;
834 std::vector<Expr>& kids = ev.
getKids1();
835 kids.push_back(child);
839 std::vector<Expr>& kids = ev.
getKids1();
840 kids.push_back(child);
850 std::vector<Expr>& kids = ev.
getKids1();
851 kids.push_back(child0);
852 kids.push_back(child1);
856 std::vector<Expr>& kids = ev.
getKids1();
857 kids.push_back(child0);
858 kids.push_back(child1);
865 const Expr& child2) {
869 std::vector<Expr>& kids = ev.
getKids1();
870 kids.push_back(child0);
871 kids.push_back(child1);
872 kids.push_back(child2);
876 std::vector<Expr>& kids = ev.
getKids1();
877 kids.push_back(child0);
878 kids.push_back(child1);
879 kids.push_back(child2);
886 const Expr& child2,
const Expr& child3) {
890 std::vector<Expr>& kids = ev.
getKids1();
891 kids.push_back(child0);
892 kids.push_back(child1);
893 kids.push_back(child2);
894 kids.push_back(child3);
898 std::vector<Expr>& kids = ev.
getKids1();
899 kids.push_back(child0);
900 kids.push_back(child1);
901 kids.push_back(child2);
902 kids.push_back(child3);
914 "Expr::Expr(Op, children): op's EM is NULL and "
915 "no children given");
916 em = children[0].getEM();
930 return Expr(
EQ, *
this, right);
942 return Expr(
AND, *
this, right);
946 DebugAssert(children.size()>0 && !children[0].isNull(),
947 "Expr::andExpr(kids)");
952 return Expr(
OR, *
this, right);
956 DebugAssert(children.size()>0 && !children[0].isNull(),
957 "Expr::andExpr(kids)");
958 return Expr(
OR, children);
962 return Expr(
ITE, *
this, thenpart, elsepart);
966 return Expr(
IFF, *
this, right);
974 return Expr(
XOR, *
this, right);
1023 if (!
getType().isBool())
return false;
1057 "CVC3::Expr::getString(): not a string Expr:\n "
1064 "CVC3::Expr::getVars(): not a closure Expr:\n "
1071 "CVC3::Expr::getBody(): not a closure Expr:\n "
1078 "CVC3::Expr::setTriggers(): not a closure Expr:\n "
1085 "CVC3::Expr::setTriggers(): not a closure Expr:\n "
1087 std::vector<std::vector<Expr> > patternvv;
1088 for(std::vector<Expr>::const_iterator i = triggers.begin(); i != triggers.end(); ++i ) {
1089 std::vector<Expr> patternv;
1090 patternv.push_back(*i);
1091 patternvv.push_back(patternv);
1098 "CVC3::Expr::setTrigger(): not a closure Expr:\n "
1100 std::vector<std::vector<Expr> > patternvv;
1101 std::vector<Expr> patternv;
1102 patternv.push_back(trigger);
1103 patternvv.push_back(patternv);
1109 "CVC3::Expr::setTrigger(): not a closure Expr:\n "
1111 std::vector<std::vector<Expr> > patternvv;
1112 patternvv.push_back(multiTrigger);
1118 "CVC3::Expr::getTrigs(): not a closure Expr:\n "
1125 "CVC3::Expr::getExistential() not a skolem variable");
1130 "CVC3::Expr::getBoundIndex() not a skolem variable");
1137 "CVC3::Expr::getRational(): not a rational Expr:\n "
1144 "CVC3::Expr::getTheorem(): not a Theorem Expr:\n "
1151 "CVC3::Expr::getUid(): not a BOUND_VAR Expr:\n "
1158 "CVC3::Expr:getEM: on Null Expr (not initialized)");
1187 "Expr::getOp() called on non-apply expr with no children");
1255 if(
isNull())
return NULL;
1412 IF_DEBUG(tmp->setName(
"CDO[Expr.find]");)
1423 IF_DEBUG(tmp->setName(
"CDO[Expr.eqNext]");)
1459 TRACE(
"setRewriteNormal",
"setRewriteNormal(", *
this,
")");
1581 if(sig != NULL) sig->
set(e);
1592 if(rep != NULL) rep->
set(e);
1600 inline bool operator==(
const Expr& e1,
const Expr& e2) {
1606 {
return !(e1 == e2); }
1611 {
return compare(e1,e2) < 0; }
1613 {
return compare(e1,e2) <= 0; }
1615 {
return compare(e1,e2) > 0; }
1617 {
return compare(e1,e2) >= 0; }