/*****************************************************************************/
/*!
* \file expr.h
* \brief Definition of the API to expression package. See class Expr for details.
*
* Author: Clark Barrett
*
* Created: Tue Nov 26 00:27:40 2002
*
* <hr>
*
* License to use, copy, modify, sell and/or distribute this software
* and its documentation for any purpose is hereby granted without
* royalty, subject to the terms and conditions defined in the \ref
* LICENSE file provided with this distribution.
*
* <hr>
*
*/
/*****************************************************************************/
#ifndef _cvc3__expr_h_
#define _cvc3__expr_h_
#include <stdlib.h>
#include <sstream>
#include <set>
#include <functional>
#include <iterator>
#include <map>
#include "os.h"
#include "compat_hash_map.h"
#include "compat_hash_set.h"
#include "rational.h"
#include "kinds.h"
#include "cdo.h"
#include "cdflags.h"
#include "lang.h"
#include "memory_manager.h"
class CInterface;
namespace CVC3 {
class NotifyList;
class Theory;
class Op;
class Type;
class Theorem;
template<class Data>
class ExprHashMap;
class ExprManager;
// Internal data-holding classes
class ExprValue;
class ExprNode;
// Printing
class ExprStream;
//! Type ID of each ExprValue subclass.
/*! It is defined in expr.h, so that ExprManager can use it before loading
expr_value.h */
typedef enum {
EXPR_VALUE,
EXPR_NODE,
EXPR_APPLY, //!< Application of functions and predicates
EXPR_STRING,
EXPR_RATIONAL,
EXPR_SKOLEM,
EXPR_UCONST,
EXPR_SYMBOL,
EXPR_BOUND_VAR,
EXPR_CLOSURE,
EXPR_THEOREM,
EXPR_VALUE_TYPE_LAST // The end of list; don't assign it to any subclass
} ExprValueType;
//! Expression index type
typedef long long unsigned ExprIndex;
/**************************************************************************/
/*! \defgroup ExprPkg Expression Package
* \ingroup BuildingBlocks
*/
/**************************************************************************/
/*! \defgroup Expr_SmartPointer Smart Pointer Functionality in Expr
* \ingroup ExprPkg
*/
/**************************************************************************/
/**************************************************************************/
//! Data structure of expressions in CVC3
/*! \ingroup ExprPkg
* Class: Expr <br>
* Author: Clark Barrett <br>
* Created: Mon Nov 25 15:29:37 2002
*
* This class is the main data structure for expressions that all
* other components should use. It is actually a <em>smart
* pointer</em> to the actual data holding class ExprValue and its
* subclasses.
*
* Expressions are represented as DAGs with maximal sharing of
* subexpressions. Therefore, testing for equality is a constant time
* operation (simply compare the pointers).
*
* Unused expressions are automatically garbage-collected. The use is
* determined by a reference counting mechanism. In particular, this
* means that if there is a circular dependency among expressions
* (e.g. an attribute points back to the expression itself), these
* expressions will not be garbage-collected, even if no one else is
* using them.
*
* The most frequently used operations are getKind() (determining the
* kind of the top level node of the expression), arity() (how many
* children an Expr has), operator[]() for accessing a child, and
* various testers and methods for constructing new expressions.
*
* In addition, a total ordering operator<() is provided. It is
* guaranteed to remain the same for the lifetime of the expressions
* (it may change, however, if the expression is garbage-collected and
* reborn).
*/
/**************************************************************************/
class CVC_DLL Expr {
friend class ExprHasher;
friend class ExprManager;
friend class Op;
friend class ExprValue;
friend class ExprNode;
friend class ::CInterface;
friend class Theorem;
/*! \addtogroup ExprPkg
* @{
*/
//! bit-masks for static flags
typedef enum {
//! Whether is valid TYPE expr
VALID_TYPE = 0x1,
//! Whether IS_ATOMIC flag is valid (initialized)
VALID_IS_ATOMIC = 0x2,
//! Whether the expression is an atomic term or formula
IS_ATOMIC = 0x4,
//! Expression is the result of a "normal" (idempotent) rewrite
REWRITE_NORMAL = 0x8,
//! Finite type
IS_FINITE = 0x400,
//! Well-founded (used in datatypes)
WELL_FOUNDED = 0x800,
//! Compute transitive closure (for binary uninterpreted predicates)
COMPUTE_TRANS_CLOSURE = 0x1000,
//! Whether expr contains a bounded variable (for quantifier instantiation)
CONTAINS_BOUND_VAR = 0x00020000
} StaticFlagsEnum;
//! bit-masks for dynamic flags
// TODO: Registered flags instead of hard-wired
typedef enum {
//! Whether expr has been added as an implied literal
IMPLIED_LITERAL = 0x10,
IS_USER_ASSUMPTION = 0x20,
IS_INT_ASSUMPTION = 0x40,
IS_JUSTIFIED = 0x80,
IS_TRANSLATED = 0x100,
IS_USER_REGISTERED_ATOM = 0x200,
IS_SELECTED = 0x2000,
IS_STORED_PREDICATE = 0x4000,
IS_REGISTERED_ATOM = 0x8000,
IN_USER_ASSUMPTION = 0x00010000
} DynamicFlagsEnum;
//! Convenient null expr
static Expr s_null;
/////////////////////////////////////////////////////////////////////////////
// Private Dynamic Data //
/////////////////////////////////////////////////////////////////////////////
//! The value. This is the only data member in this class.
ExprValue* d_expr;
/////////////////////////////////////////////////////////////////////////////
// Private methods //
/////////////////////////////////////////////////////////////////////////////
//! Private constructor, simply wraps around the pointer
Expr(ExprValue* expr);
Expr recursiveSubst(const ExprHashMap<Expr>& subst,
ExprHashMap<Expr>& visited) const;
public:
/////////////////////////////////////////////////////////////////////////////
// Public Classes and Types //
/////////////////////////////////////////////////////////////////////////////
/////////////////////////////////////////////////////////////////////////////
/*!
* Class: Expr::iterator
* Author: Sergey Berezin
* Created: Fri Dec 6 15:38:51 2002
* Description: STL-like iterator API to the Expr's children.
* IMPORTANT: the iterator will not be valid after the originating
* expression is destroyed.
*/
/////////////////////////////////////////////////////////////////////////////
class CVC_DLL iterator
: public std::iterator<std::input_iterator_tag,Expr,ptrdiff_t>
{
friend class Expr;
private:
std::vector<Expr>::const_iterator d_it;
// Private constructors (used by Expr only)
//
//! Construct an iterator out of the vector's iterator
iterator(std::vector<Expr>::const_iterator it): d_it(it) { }
// Public methods
public:
//! Default constructor
iterator() { }
// Copy constructor and operator= are defined by C++, that's good enough
//! Equality
bool operator==(const iterator& i) const {
return d_it == i.d_it;
}
//! Disequality
bool operator!=(const iterator& i) const { return !(*this == i); }
//! Dereference operator
const Expr& operator*() const { return *d_it; }
//! Dereference and member access
const Expr* operator->() const { return &(operator*()); }
//! Prefix increment
iterator& operator++() {
d_it++;
return *this;
}
/*! @brief Postfix increment requires a Proxy object to hold the
* intermediate value for dereferencing */
class Proxy {
const Expr* d_e;
public:
Proxy(const Expr& e) : d_e(&e) { }
Expr operator*() { return *d_e; }
};
//! Postfix increment
/*! \return Proxy with the old Expr.
*
* Now, an expression like *i++ will return the current *i, and
* then advance the iterator. However, don't try to use Proxy for
* anything else.
*/
Proxy operator++(int) {
Proxy e(*(*this));
++(*this);
return e;
}
}; // end of class Expr::iterator
/////////////////////////////////////////////////////////////////////////////
// Constructors //
/////////////////////////////////////////////////////////////////////////////
//! Default constructor creates the Null Expr
Expr(): d_expr(NULL) {}
/*! @brief Copy constructor and assignment (copy the pointer and take care
of the refcount) */
Expr(const Expr& e);
//! Assignment operator: take care of the refcounting and GC
Expr& operator=(const Expr& e);
// These constructors grab the ExprManager from the Op or the first
// child. The operator and all children must belong to the same
// ExprManager.
Expr(const Op& op, const Expr& child);
Expr(const Op& op, const Expr& child0, const Expr& child1);
Expr(const Op& op, const Expr& child0, const Expr& child1,
const Expr& child2);
Expr(const Op& op, const Expr& child0, const Expr& child1,
const Expr& child2, const Expr& child3);
Expr(const Op& op, const std::vector<Expr>& children,
ExprManager* em = NULL);
//! Destructor
~Expr();
// Compound expression constructors
Expr eqExpr(const Expr& right) const;
Expr notExpr() const;
Expr negate() const; // avoid double-negatives
Expr andExpr(const Expr& right) const;
Expr orExpr(const Expr& right) const;
Expr iteExpr(const Expr& thenpart, const Expr& elsepart) const;
Expr iffExpr(const Expr& right) const;
Expr impExpr(const Expr& right) const;
//! Create a Skolem constant for the i'th variable of an existential (*this)
Expr skolemExpr(int i) const;
//! Create a Boolean variable out of the expression
// Expr boolVarExpr() const;
//! Rebuild Expr with a new ExprManager
Expr rebuild(ExprManager* em) const;
// Expr newForall(const Expr& e);
// Expr newExists(const Expr& e);
Expr substExpr(const std::vector<Expr>& oldTerms,
const std::vector<Expr>& newTerms) const;
Expr substExpr(const ExprHashMap<Expr>& oldToNew) const;
Expr operator!() const { return notExpr(); }
Expr operator&&(const Expr& right) const { return andExpr(right); }
Expr operator||(const Expr& right) const { return orExpr(right); }
/////////////////////////////////////////////////////////////////////////////
// Public Static Methods //
/////////////////////////////////////////////////////////////////////////////
static size_t hash(const Expr& e);
/////////////////////////////////////////////////////////////////////////////
// Read-only (const) methods //
/////////////////////////////////////////////////////////////////////////////
size_t hash() const;
// Core expression testers
bool isFalse() const { return getKind() == FALSE_EXPR; }
bool isTrue() const { return getKind() == TRUE_EXPR; }
bool isBoolConst() const { return isFalse() || isTrue(); }
bool isVar() const;
bool isBoundVar() const { return getKind() == BOUND_VAR; }
bool isString() const;
bool isClosure() const;
bool isQuantifier() const;
bool isLambda() const;
bool isApply() const;
bool isSymbol() const;
bool isTheorem() const;
//! Expr represents a type
bool isType() const;
/*
bool isRecord() const;
bool isRecordAccess() const;
bool isTupleAccess() const;
*/
//! Provide access to ExprValue for client subclasses of ExprValue *only*
/*@ Calling getExprValue on an Expr with a built-in ExprValue class will
* cause an error */
const ExprValue* getExprValue() const;
//! Test if e is a term (as opposed to a predicate/formula)
bool isTerm() const;
//! Test if e is atomic
/*! An atomic expression is one that does not contain a formula (including
* not being a formula itself).
* \sa isAtomicFormula */
bool isAtomic() const;
//! Test if e is an atomic formula
/*! An atomic formula is TRUE or FALSE or an application of a predicate
(possibly 0-ary) which does not properly contain any formula. For
instance, the formula "x = IF f THEN y ELSE z ENDIF is not an atomic
formula, since it contains the condition "f", which is a formula. */
bool isAtomicFormula() const;
//! An abstract atomic formua is an atomic formula or a quantified formula
bool isAbsAtomicFormula() const
{ return isQuantifier() || isAtomicFormula(); }
//! Test if e is a literal
/*! A literal is an atomic formula, or its negation.
\sa isAtomicFormula */
bool isLiteral() const
{ return (isAtomicFormula() || (isNot() && (*this)[0].isAtomicFormula())); }
//! Test if e is an abstract literal
bool isAbsLiteral() const
{ return (isAbsAtomicFormula() || (isNot() && (*this)[0].isAbsAtomicFormula())); }
//! A Bool connective is one of NOT,AND,OR,IMPLIES,IFF,XOR,ITE (with type Bool)
bool isBoolConnective() const;
//! True iff expr is not a Bool connective
bool isPropAtom() const { return !isBoolConnective(); }
//! PropAtom or negation of PropAtom
bool isPropLiteral() const
{ return (isNot() && (*this)[0].isPropAtom()) || isPropAtom(); }
bool isEq() const { return getKind() == EQ; }
bool isNot() const { return getKind() == NOT; }
bool isAnd() const { return getKind() == AND; }
bool isOr() const { return getKind() == OR; }
bool isITE() const { return getKind() == ITE; }
bool isIff() const { return getKind() == IFF; }
bool isImpl() const { return getKind() == IMPLIES; }
bool isXor() const { return getKind() == XOR;}
bool isForall() const { return getKind() == FORALL; }
bool isExists() const { return getKind() == EXISTS; }
bool isRational() const { return getKind() == RATIONAL_EXPR; }
bool isSkolem() const { return getKind() == SKOLEM_VAR;}
// Leaf accessors - these functions must only be called one expressions of
// the appropriate kind.
// For UCONST and BOUND_VAR Expr's
const std::string& getName() const;
//! For BOUND_VAR, get the UID
const std::string& getUid() const;
// For STRING_EXPR's
const std::string& getString() const;
//! Get bound variables from a closure Expr
const std::vector<Expr>& getVars() const;
//! Get the existential axiom expression for skolem constant
const Expr& getExistential() const;
//! Get the index of the bound var that skolem constant comes from
int getBoundIndex() const;
//! Get the body of the closure Expr
const Expr& getBody() const;
//! Get the Rational value out of RATIONAL_EXPR
const Rational& getRational() const;
//! Get theorem from THEOREM_EXPR
const Theorem& getTheorem() const;
// Get the expression manager. The expression must be non-null.
ExprManager *getEM() const;
// Return a ref to the vector of children.
const std::vector<Expr>& getKids() const;
// Get the kind of this expr.
int getKind() const;
// Get the index field
ExprIndex getIndex() const;
// True if this is the most recently created expression
bool hasLastIndex() const;
//! Make the expr into an operator
Op mkOp() const;
//! Get operator from expression
Op getOp() const;
//! Get expression of operator (for APPLY Exprs only)
Expr getOpExpr() const;
//! Get kind of operator (for APPLY Exprs only)
int getOpKind() const;
// Return the number of children. Note, that an application of a
// user-defined function has the arity of that function (the number
// of arguments), and the function name itself is part of the
// operator.
int arity() const;
// Return the ith child. As with arity, it's also the ith argument
// in function application.
const Expr& operator[](int i) const;
//! Remove leading NOT if any
const Expr& unnegate() const { return isNot() ? (*this)[0] : *this; }
//! Begin iterator
iterator begin() const;
//! End iterator
iterator end() const;
// Check if Expr is Null
bool isNull() const;
// Check if Expr is not Null
bool isInitialized() const { return d_expr != NULL; }
//! Get the memory manager index (it uniquely identifies the subclass)
size_t getMMIndex() const;
// Attributes
// True if the find attribute has been set to something other than NULL.
bool hasFind() const;
// Return the attached find attribute for the expr. Note that this
// must be called repeatedly to get the root of the union-find tree.
// Should only be called if hasFind is true.
const Theorem& getFind() const;
int getFindLevel() const;
// Return the notify list
NotifyList* getNotify() const;
//! Get the type. Recursively compute if necessary
const Type getType() const;
//! Look up the current type. Do not recursively compute (i.e. may be NULL)
const Type lookupType() const;
/*! @brief Return true if there is a valid cached value for calling
simplify on this Expr. */
bool validSimpCache() const;
// Get the cached Simplify of this Expr.
const Theorem& getSimpCache() const;
// Return true if valid type flag is set for Expr
bool isValidType() const;
// Return true if there is a valid flag for whether Expr is atomic
bool validIsAtomicFlag() const;
// Get the isAtomic flag
bool getIsAtomicFlag() const;
// Get the RewriteNormal flag
bool isRewriteNormal() const;
// Get the isFinite flag
bool isFinite() const;
// Get the WellFounded flag
bool isWellFounded() const;
// Get the ComputeTransClosure flag
bool computeTransClosure() const;
// Get the ContainsBoundVar flag
bool containsBoundVar() const;
// Get the ImpliedLiteral flag
bool isImpliedLiteral() const;
// Get the UserAssumption flag
bool isUserAssumption() const;
// Get the inUserAssumption flag
bool inUserAssumption() const;
// Get the IntAssumption flag
bool isIntAssumption() const;
// Get the Justified flag
bool isJustified() const;
// Get the Translated flag
bool isTranslated() const;
// Get the UserRegisteredAtom flag
bool isUserRegisteredAtom() const;
// Get the RegisteredAtom flag
bool isRegisteredAtom() const;
// Get the Selected flag
bool isSelected() const;
// Get the Stored Predicate flag
bool isStoredPredicate() const;
//! Check if the generic flag is set
bool getFlag() const;
//! Set the generic flag
void setFlag() const;
//! Clear the generic flag in all Exprs
void clearFlags() const;
// Printing functions
//! Print the expression to a string
std::string toString() const;
//! Print the expression to a string using the given output language
std::string toString(InputLanguage lang) const;
//! Print the expression in the specified format
void print(InputLanguage lang, bool dagify = true) const;
//! Print the expression as AST (lisp-like format)
void print() const { print(AST_LANG); }
//! Print the expression as AST without dagifying
void printnodag() const;
//! Pretty-print the expression
void pprint() const;
//! Pretty-print without dagifying
void pprintnodag() const;
//! Print a leaf node
/*@ The top node is pretty-printed if it is a basic leaf type;
* otherwise, just the kind is printed. Should only be called on expressions
* with no children. */
ExprStream& print(ExprStream& os) const;
//! Print the top node and then recurse through the children */
/*@ The top node is printed as an AST with all the information, including
* "hidden" Exprs that are part of the ExprValue */
ExprStream& printAST(ExprStream& os) const;
//! Set initial indentation to n.
/*! The indentation will be reset to default unless the second
argument is true.
\return reference to itself, so one can write `os << e.indent(5)'
*/
Expr& indent(int n, bool permanent = false);
/////////////////////////////////////////////////////////////////////////////
// Other Public methods //
/////////////////////////////////////////////////////////////////////////////
// Attributes
//! Set the find attribute to e
void setFind(const Theorem& e) const;
//! Add (e,i) to the notify list of this expression
void addToNotify(Theory* i, const Expr& e) const;
//! Set the cached type
void setType(const Type& t) const;
// Cache the result of a call to Simplify on this Expr
void setSimpCache(const Theorem& e) const;
// Set the valid type flag for this Expr
void setValidType() const;
// Set the isAtomicFlag for this Expr
void setIsAtomicFlag(bool value) const;
// Set or clear the RewriteNormal flag
void setRewriteNormal() const;
void clearRewriteNormal() const;
// Set the isFinite flag
void setFinite() const;
// Set the WellFounded flag
void setWellFounded() const;
// Set the ComputeTransClosure flag
void setComputeTransClosure() const;
// Set the ContainsBoundVar flag
void setContainsBoundVar() const;
// Set the impliedLiteral flag for this Expr
void setImpliedLiteral() const;
// Set the user assumption flag for this Expr
void setUserAssumption(int scope = -1) const;
// Set the in user assumption flag for this Expr
void setInUserAssumption(int scope = -1) const;
// Set the internal assumption flag for this Expr
void setIntAssumption() const;
// Set the justified flag for this Expr
void setJustified() const;
//! Set the translated flag for this Expr
void setTranslated(int scope = -1) const;
//! Set the UserRegisteredAtom flag for this Expr
void setUserRegisteredAtom() const;
//! Set the RegisteredAtom flag for this Expr
void setRegisteredAtom() const;
//! Set the Selected flag for this Expr
void setSelected() const;
//! Set the Stored Predicate flag for this Expr
void setStoredPredicate() const;
//! Check if the current Expr (*this) is a subexpression of e
bool subExprOf(const Expr& e) const;
// Returns the maximum number of Boolean expressions on a path from
// this to a leaf, including this.
// inline int getHeight() const;
// // Returns the index of the highest kid.
// inline int getHighestKid() const;
// // Gets/sets an expression that this expression was simplified from
// // (see newRWTheorem). This is the equivalent of SVC's Sigx.
// inline bool hasSimpFrom() const;
// inline const Expr& getSimpFrom() const;
// inline void setSimpFrom(const Expr& simpFrom);
// Attributes for uninterpreted function symbols.
bool hasSig() const;
bool hasRep() const;
const Theorem& getSig() const;
const Theorem& getRep() const;
void setSig(const Theorem& e) const;
void setRep(const Theorem& e) const;
/////////////////////////////////////////////////////////////////////////////
// Friend methods //
/////////////////////////////////////////////////////////////////////////////
friend CVC_DLL std::ostream& operator<<(std::ostream& os, const Expr& e);
// The master method which defines some fixed total ordering on all
// Exprs. If e1 < e2, e1==e2, and e1 > e2, it returns -1, 0, 1
// respectively. A Null expr is always "smaller" than any other
// expr, but is equal to itself.
friend int compare(const Expr& e1, const Expr& e2);
friend bool operator==(const Expr& e1, const Expr& e2);
friend bool operator!=(const Expr& e1, const Expr& e2);
friend bool operator<(const Expr& e1, const Expr& e2);
friend bool operator<=(const Expr& e1, const Expr& e2);
friend bool operator>(const Expr& e1, const Expr& e2);
friend bool operator>=(const Expr& e1, const Expr& e2);
/*!@}*/ // end of group Expr
}; // end of class Expr
} // end of namespace CVC3
// Include expr_value.h here. We cannot include it earlier, since it
// needs the definition of class Expr. See comments in expr_value.h.
#ifndef DOXYGEN
#include "expr_op.h"
#include "expr_manager.h"
#endif
namespace CVC3 {
inline Expr::Expr(ExprValue* expr) : d_expr(expr) { d_expr->incRefcount(); }
inline Expr::Expr(const Expr& e) : d_expr(e.d_expr) {
if (d_expr != NULL) d_expr->incRefcount();
}
inline Expr& Expr::operator=(const Expr& e) {
if(&e == this) return *this; // Self-assignment
ExprValue* tmp = e.d_expr;
if (tmp == NULL) {
if (d_expr == NULL) {
return *this;
}
d_expr->decRefcount();
}
else {
tmp->incRefcount();
if(d_expr != NULL) {
d_expr->decRefcount();
}
}
d_expr = tmp;
return *this;
}
inline Expr::Expr(const Op& op, const Expr& child) {
ExprManager* em = child.getEM();
if (op.getExpr().isNull()) {
ExprNode ev(em, op.getKind());
std::vector<Expr>& kids = ev.getKids1();
kids.push_back(child);
d_expr = em->newExprValue(&ev);
} else {
ExprApply ev(em, op);
std::vector<Expr>& kids = ev.getKids1();
kids.push_back(child);
d_expr = em->newExprValue(&ev);
}
d_expr->incRefcount();
}
inline Expr::Expr(const Op& op, const Expr& child0, const Expr& child1) {
ExprManager* em = child0.getEM();
if (op.getExpr().isNull()) {
ExprNode ev(em, op.getKind());
std::vector<Expr>& kids = ev.getKids1();
kids.push_back(child0);
kids.push_back(child1);
d_expr = em->newExprValue(&ev);
} else {
ExprApply ev(em, op);
std::vector<Expr>& kids = ev.getKids1();
kids.push_back(child0);
kids.push_back(child1);
d_expr = em->newExprValue(&ev);
}
d_expr->incRefcount();
}
inline Expr::Expr(const Op& op, const Expr& child0, const Expr& child1,
const Expr& child2) {
ExprManager* em = child0.getEM();
if (op.getExpr().isNull()) {
ExprNode ev(em, op.getKind());
std::vector<Expr>& kids = ev.getKids1();
kids.push_back(child0);
kids.push_back(child1);
kids.push_back(child2);
d_expr = em->newExprValue(&ev);
} else {
ExprApply ev(em, op);
std::vector<Expr>& kids = ev.getKids1();
kids.push_back(child0);
kids.push_back(child1);
kids.push_back(child2);
d_expr = em->newExprValue(&ev);
}
d_expr->incRefcount();
}
inline Expr::Expr(const Op& op, const Expr& child0, const Expr& child1,
const Expr& child2, const Expr& child3) {
ExprManager* em = child0.getEM();
if (op.getExpr().isNull()) {
ExprNode ev(em, op.getKind());
std::vector<Expr>& kids = ev.getKids1();
kids.push_back(child0);
kids.push_back(child1);
kids.push_back(child2);
kids.push_back(child3);
d_expr = em->newExprValue(&ev);
} else {
ExprApply ev(em, op);
std::vector<Expr>& kids = ev.getKids1();
kids.push_back(child0);
kids.push_back(child1);
kids.push_back(child2);
kids.push_back(child3);
d_expr = em->newExprValue(&ev);
}
d_expr->incRefcount();
}
inline Expr::Expr(const Op& op, const std::vector<Expr>& children,
ExprManager* em) {
if (em == NULL) {
if (!op.getExpr().isNull()) em = op.getExpr().getEM();
else {
DebugAssert(children.size() > 0,
"Expr::Expr(Op, children): op's EM is NULL and "
"no children given");
em = children[0].getEM();
}
}
if (op.getExpr().isNull()) {
ExprNodeTmp ev(em, op.getKind(), children);
d_expr = em->newExprValue(&ev);
} else {
ExprApplyTmp ev(em, op, children);
d_expr = em->newExprValue(&ev);
}
d_expr->incRefcount();
}
inline Expr Expr::eqExpr(const Expr& right) const {
return Expr(EQ, *this, right);
}
inline Expr Expr::notExpr() const {
return Expr(NOT, *this);
}
inline Expr Expr::negate() const {
return isNot() ? (*this)[0] : this->notExpr();
}
inline Expr Expr::andExpr(const Expr& right) const {
return Expr(AND, *this, right);
}
inline Expr andExpr(const std::vector <Expr>& children) {
DebugAssert(children.size()>0 && !children[0].isNull(),
"Expr::andExpr(kids)");
return Expr(AND, children);
}
inline Expr Expr::orExpr(const Expr& right) const {
return Expr(OR, *this, right);
}
inline Expr orExpr(const std::vector <Expr>& children) {
DebugAssert(children.size()>0 && !children[0].isNull(),
"Expr::andExpr(kids)");
return Expr(OR, children);
}
inline Expr Expr::iteExpr(const Expr& thenpart, const Expr& elsepart) const {
return Expr(ITE, *this, thenpart, elsepart);
}
inline Expr Expr::iffExpr(const Expr& right) const {
return Expr(IFF, *this, right);
}
inline Expr Expr::impExpr(const Expr& right) const {
return Expr(IMPLIES, *this, right);
}
inline Expr Expr::skolemExpr(int i) const {
return getEM()->newSkolemExpr(*this, i);
}
inline Expr Expr::rebuild(ExprManager* em) const {
return em->rebuild(*this);
}
inline Expr::~Expr() {
if(d_expr != NULL) {
d_expr->decRefcount();
}
}
inline size_t Expr::hash(const Expr& e) { return e.getEM()->hash(e); }
/////////////////////////////////////////////////////////////////////////////
// Read-only (const) methods //
/////////////////////////////////////////////////////////////////////////////
inline size_t Expr::hash() const { return getEM()->hash(*this); }
inline const ExprValue* Expr::getExprValue() const
{ return d_expr->getExprValue(); }
// Core Expression Testers
inline bool Expr::isVar() const { return d_expr->isVar(); }
inline bool Expr::isString() const { return d_expr->isString(); }
inline bool Expr::isClosure() const { return d_expr->isClosure(); }
inline bool Expr::isQuantifier() const {
return (isClosure() && (getKind() == FORALL || getKind() == EXISTS));
}
inline bool Expr::isLambda() const {
return (isClosure() && getKind() == LAMBDA);
}
inline bool Expr::isApply() const
{ DebugAssert((getKind() != APPLY || d_expr->isApply()) &&
(!d_expr->isApply() || getKind() == APPLY), "APPLY mismatch");
return d_expr->isApply(); }
inline bool Expr::isSymbol() const { return d_expr->isSymbol(); }
inline bool Expr::isTheorem() const { return d_expr->isTheorem(); }
inline bool Expr::isType() const { return getEM()->isTypeKind(getOpKind()); }
inline bool Expr::isTerm() const { return !getType().isBool(); }
inline bool Expr::isBoolConnective() const {
if (!getType().isBool()) return false;
switch (getKind()) {
case NOT: case AND: case OR: case IMPLIES: case IFF: case XOR: case ITE:
return true; }
return false;
}
//inline int Expr::getHeight() const { return d_expr->getHeight(); }
//inline int Expr::getHighestKid() const { return d_expr->getHighestKid(); }
//inline bool Expr::hasSimpFrom() const
// { return !d_expr->getSimpFrom().isNull(); }
// inline const Expr& Expr::getSimpFrom() const
// { return hasSimpFrom() ? d_expr->getSimpFrom() : *this; }
// inline void Expr::setSimpFrom(const Expr& simpFrom)
// { d_expr->setSimpFrom(simpFrom); }
// Leaf accessors
inline const std::string& Expr::getName() const {
DebugAssert(!isNull(), "Expr::getName() on Null expr");
return d_expr->getName();
}
inline const std::string& Expr::getString() const {
DebugAssert(isString(),
"CVC3::Expr::getString(): not a string Expr:\n "
+ toString(AST_LANG));
return d_expr->getString();
}
inline const std::vector<Expr>& Expr::getVars() const {
DebugAssert(isClosure(),
"CVC3::Expr::getVars(): not a closure Expr:\n "
+ toString(AST_LANG));
return d_expr->getVars();
}
inline const Expr& Expr::getBody() const {
DebugAssert(isClosure(),
"CVC3::Expr::getBody(): not a closure Expr:\n "
+ toString(AST_LANG));
return d_expr->getBody();
}
inline const Expr& Expr::getExistential() const {
DebugAssert(isSkolem(),
"CVC3::Expr::getExistential() not a skolem variable");
return d_expr->getExistential();
}
inline int Expr::getBoundIndex() const {
DebugAssert(isSkolem(),
"CVC3::Expr::getBoundIndex() not a skolem variable");
return d_expr->getBoundIndex();
}
inline const Rational& Expr::getRational() const {
DebugAssert(isRational(),
"CVC3::Expr::getRational(): not a rational Expr:\n "
+ toString(AST_LANG));
return d_expr->getRational();
}
inline const Theorem& Expr::getTheorem() const {
DebugAssert(isTheorem(),
"CVC3::Expr::getTheorem(): not a Theorem Expr:\n "
+ toString(AST_LANG));
return d_expr->getTheorem();
}
inline const std::string& Expr::getUid() const {
DebugAssert(getKind() == BOUND_VAR,
"CVC3::Expr::getUid(): not a BOUND_VAR Expr:\n "
+ toString(AST_LANG));
return d_expr->getUid();
}
inline ExprManager* Expr::getEM() const {
DebugAssert(d_expr != NULL,
"CVC3::Expr:getEM: on Null Expr (not initialized)");
return d_expr->d_em;
}
inline const std::vector<Expr>& Expr::getKids() const {
DebugAssert(d_expr != NULL, "Expr::getKids on Null Expr");
if(isNull()) return getEM()->getEmptyVector();
else return d_expr->getKids();
}
inline int Expr::getKind() const {
if(d_expr == NULL) return NULL_KIND; // FIXME: invent a better Null kind
return d_expr->d_kind;
}
inline ExprIndex Expr::getIndex() const { return d_expr->d_index; }
inline bool Expr::hasLastIndex() const
{ return d_expr->d_em->lastIndex() == getIndex(); }
inline Op Expr::mkOp() const {
DebugAssert(!isNull(), "Expr::mkOp() on Null expr");
return Op(*this);
}
inline Op Expr::getOp() const {
DebugAssert(!isNull(), "Expr::getOp() on Null expr");
if (isApply()) return d_expr->getOp();
DebugAssert(arity() > 0,
"Expr::getOp() called on non-apply expr with no children");
return Op(getKind());
}
inline Expr Expr::getOpExpr() const {
DebugAssert(isApply(), "getOpExpr() called on non-apply");
return getOp().getExpr();
}
inline int Expr::getOpKind() const {
if (!isApply()) return getKind();
return getOp().getExpr().getKind();
}
inline int Expr::arity() const {
if(isNull()) return 0;
else return d_expr->arity();
}
inline const Expr& Expr::operator[](int i) const {
DebugAssert(i < arity(), "out of bounds access");
return (d_expr->getKids())[i];
}
inline Expr::iterator Expr::begin() const {
if (isNull() || d_expr->arity() == 0)
return Expr::iterator(getEM()->getEmptyVector().begin());
else return Expr::iterator(d_expr->getKids().begin());
}
inline Expr::iterator Expr::end() const {
if (isNull() || d_expr->arity() == 0)
return Expr::iterator(getEM()->getEmptyVector().end());
else return Expr::iterator(d_expr->getKids().end());
}
inline bool Expr::isNull() const {
return (d_expr == NULL) || (d_expr->d_kind == NULL_KIND);
}
inline size_t Expr::getMMIndex() const {
DebugAssert(!isNull(), "Expr::getMMIndex()");
return d_expr->getMMIndex();
}
inline bool Expr::hasFind() const {
DebugAssert(!isNull(), "hasFind called on NULL Expr");
return (d_expr->d_find && !(d_expr->d_find->get().isNull()));
}
inline const Theorem& Expr::getFind() const {
DebugAssert(hasFind(), "Should only be called if find is valid");
return d_expr->d_find->get();
}
inline int Expr::getFindLevel() const {
DebugAssert(hasFind(), "Should only be called if find is valid");
return d_expr->d_find->level();
}
inline NotifyList* Expr::getNotify() const {
if(isNull()) return NULL;
else return d_expr->d_notifyList;
}
inline const Type Expr::getType() const {
if (isNull()) return s_null;
if(d_expr->d_type.isNull()) getEM()->computeType(*this);
return d_expr->d_type;
}
inline const Type Expr::lookupType() const {
if (isNull()) return s_null;
return d_expr->d_type;
}
inline bool Expr::validSimpCache() const {
return d_expr->d_simpCacheTag == getEM()->getSimpCacheTag();
}
inline const Theorem& Expr::getSimpCache() const {
return d_expr->d_simpCache;
}
inline bool Expr::isValidType() const {
return d_expr->d_dynamicFlags.get(VALID_TYPE);
}
inline bool Expr::validIsAtomicFlag() const {
return d_expr->d_dynamicFlags.get(VALID_IS_ATOMIC);
}
inline bool Expr::getIsAtomicFlag() const {
return d_expr->d_dynamicFlags.get(IS_ATOMIC);
}
inline bool Expr::isRewriteNormal() const {
return d_expr->d_dynamicFlags.get(REWRITE_NORMAL);
}
inline bool Expr::isFinite() const {
return d_expr->d_dynamicFlags.get(IS_FINITE);
}
inline bool Expr::isWellFounded() const {
return d_expr->d_dynamicFlags.get(WELL_FOUNDED);
}
inline bool Expr::computeTransClosure() const {
return d_expr->d_dynamicFlags.get(COMPUTE_TRANS_CLOSURE);
}
inline bool Expr::containsBoundVar() const {
return d_expr->d_dynamicFlags.get(CONTAINS_BOUND_VAR);
}
inline bool Expr::isImpliedLiteral() const {
return d_expr->d_dynamicFlags.get(IMPLIED_LITERAL);
}
inline bool Expr::isUserAssumption() const {
return d_expr->d_dynamicFlags.get(IS_USER_ASSUMPTION);
}
inline bool Expr::inUserAssumption() const {
return d_expr->d_dynamicFlags.get(IN_USER_ASSUMPTION);
}
inline bool Expr::isIntAssumption() const {
return d_expr->d_dynamicFlags.get(IS_INT_ASSUMPTION);
}
inline bool Expr::isJustified() const {
return d_expr->d_dynamicFlags.get(IS_JUSTIFIED);
}
inline bool Expr::isTranslated() const {
return d_expr->d_dynamicFlags.get(IS_TRANSLATED);
}
inline bool Expr::isUserRegisteredAtom() const {
return d_expr->d_dynamicFlags.get(IS_USER_REGISTERED_ATOM);
}
inline bool Expr::isRegisteredAtom() const {
return d_expr->d_dynamicFlags.get(IS_REGISTERED_ATOM);
}
inline bool Expr::isSelected() const {
return d_expr->d_dynamicFlags.get(IS_SELECTED);
}
inline bool Expr::isStoredPredicate() const {
return d_expr->d_dynamicFlags.get(IS_STORED_PREDICATE);
}
inline bool Expr::getFlag() const {
DebugAssert(!isNull(), "Expr::getFlag() on Null Expr");
return (d_expr->d_flag == getEM()->getFlag());
}
inline void Expr::setFlag() const {
DebugAssert(!isNull(), "Expr::setFlag() on Null Expr");
d_expr->d_flag = getEM()->getFlag();
}
inline void Expr::clearFlags() const {
DebugAssert(!isNull(), "Expr::clearFlags() on Null Expr");
getEM()->clearFlags();
}
inline void Expr::setFind(const Theorem& e) const {
DebugAssert(!isNull(), "Expr::setFind() on Null expr");
DebugAssert(e.getLHS() == *this, "bad call to setFind");
if (d_expr->d_find) d_expr->d_find->set(e);
else {
CDO<Theorem>* tmp = new(true) CDO<Theorem>(getEM()->getCurrentContext(), e);
d_expr->d_find = tmp;
IF_DEBUG(tmp->setName("CDO[Expr.find]"));
}
}
inline void Expr::setType(const Type& t) const {
DebugAssert(!isNull(), "Expr::setType() on Null expr");
d_expr->d_type = t;
}
inline void Expr::setSimpCache(const Theorem& e) const {
DebugAssert(!isNull(), "Expr::setSimpCache() on Null expr");
d_expr->d_simpCache = e;
d_expr->d_simpCacheTag = getEM()->getSimpCacheTag();
}
inline void Expr::setValidType() const {
DebugAssert(!isNull(), "Expr::setValidType() on Null expr");
d_expr->d_dynamicFlags.set(VALID_TYPE, 0);
}
inline void Expr::setIsAtomicFlag(bool value) const {
DebugAssert(!isNull(), "Expr::setIsAtomicFlag() on Null expr");
d_expr->d_dynamicFlags.set(VALID_IS_ATOMIC, 0);
if (value) d_expr->d_dynamicFlags.set(IS_ATOMIC, 0);
else d_expr->d_dynamicFlags.clear(IS_ATOMIC, 0);
}
inline void Expr::setRewriteNormal() const {
DebugAssert(!isNull(), "Expr::setRewriteNormal() on Null expr");
TRACE("setRewriteNormal", "setRewriteNormal(", *this, ")");
d_expr->d_dynamicFlags.set(REWRITE_NORMAL, 0);
}
inline void Expr::setFinite() const {
DebugAssert(!isNull(), "Expr::setFinite() on Null expr");
d_expr->d_dynamicFlags.set(IS_FINITE, 0);
}
inline void Expr::setWellFounded() const {
DebugAssert(!isNull(), "Expr::setWellFounded() on Null expr");
d_expr->d_dynamicFlags.set(WELL_FOUNDED, 0);
}
inline void Expr::setComputeTransClosure() const {
DebugAssert(!isNull(), "Expr::setComputeTransClosure() on Null expr");
d_expr->d_dynamicFlags.set(COMPUTE_TRANS_CLOSURE, 0);
}
inline void Expr::setContainsBoundVar() const {
DebugAssert(!isNull(), "Expr::setContainsBoundVar() on Null expr");
d_expr->d_dynamicFlags.set(CONTAINS_BOUND_VAR, 0);
}
inline void Expr::setImpliedLiteral() const {
DebugAssert(!isNull(), "Expr::setImpliedLiteral() on Null expr");
d_expr->d_dynamicFlags.set(IMPLIED_LITERAL);
}
inline void Expr::setUserAssumption(int scope) const {
DebugAssert(!isNull(), "Expr::setUserAssumption() on Null expr");
d_expr->d_dynamicFlags.set(IS_USER_ASSUMPTION, scope);
}
inline void Expr::setInUserAssumption(int scope) const {
DebugAssert(!isNull(), "Expr::setInUserAssumption() on Null expr");
d_expr->d_dynamicFlags.set(IN_USER_ASSUMPTION, scope);
}
inline void Expr::setIntAssumption() const {
DebugAssert(!isNull(), "Expr::setIntAssumption() on Null expr");
d_expr->d_dynamicFlags.set(IS_INT_ASSUMPTION);
}
inline void Expr::setJustified() const {
DebugAssert(!isNull(), "Expr::setJustified() on Null expr");
d_expr->d_dynamicFlags.set(IS_JUSTIFIED);
}
inline void Expr::setTranslated(int scope) const {
DebugAssert(!isNull(), "Expr::setTranslated() on Null expr");
d_expr->d_dynamicFlags.set(IS_TRANSLATED, scope);
}
inline void Expr::setUserRegisteredAtom() const {
DebugAssert(!isNull(), "Expr::setUserRegisteredAtom() on Null expr");
d_expr->d_dynamicFlags.set(IS_USER_REGISTERED_ATOM);
}
inline void Expr::setRegisteredAtom() const {
DebugAssert(!isNull(), "Expr::setUserRegisteredAtom() on Null expr");
d_expr->d_dynamicFlags.set(IS_REGISTERED_ATOM);
}
inline void Expr::setSelected() const {
DebugAssert(!isNull(), "Expr::setSelected() on Null expr");
d_expr->d_dynamicFlags.set(IS_SELECTED);
}
inline void Expr::setStoredPredicate() const {
DebugAssert(!isNull(), "Expr::setStoredPredicate() on Null expr");
d_expr->d_dynamicFlags.set(IS_STORED_PREDICATE);
}
inline void Expr::clearRewriteNormal() const {
DebugAssert(!isNull(), "Expr::clearRewriteNormal() on Null expr");
d_expr->d_dynamicFlags.clear(REWRITE_NORMAL, 0);
}
inline bool Expr::hasSig() const {
return (!isNull()
&& d_expr->getSig() != NULL
&& !(d_expr->getSig()->get().isNull()));
}
inline bool Expr::hasRep() const {
return (!isNull()
&& d_expr->getRep() != NULL
&& !(d_expr->getRep()->get().isNull()));
}
inline const Theorem& Expr::getSig() const {
static Theorem nullThm;
DebugAssert(!isNull(), "Expr::getSig() on Null expr");
if(d_expr->getSig() != NULL)
return d_expr->getSig()->get();
else
return nullThm;
}
inline const Theorem& Expr::getRep() const {
static Theorem nullThm;
DebugAssert(!isNull(), "Expr::getRep() on Null expr");
if(d_expr->getRep() != NULL)
return d_expr->getRep()->get();
else
return nullThm;
}
inline void Expr::setSig(const Theorem& e) const {
DebugAssert(!isNull(), "Expr::setSig() on Null expr");
CDO<Theorem>* sig = d_expr->getSig();
if(sig != NULL) sig->set(e);
else {
CDO<Theorem>* tmp = new(true) CDO<Theorem>(getEM()->getCurrentContext(), e);
d_expr->setSig(tmp);
IF_DEBUG(tmp->setName("CDO[Expr.sig] in "+toString()));
}
}
inline void Expr::setRep(const Theorem& e) const {
DebugAssert(!isNull(), "Expr::setRep() on Null expr");
CDO<Theorem>* rep = d_expr->getRep();
if(rep != NULL) rep->set(e);
else {
CDO<Theorem>* tmp = new(true) CDO<Theorem>(getEM()->getCurrentContext(), e);
d_expr->setRep(tmp);
IF_DEBUG(tmp->setName("CDO[Expr.rep] in "+toString()));
}
}
inline bool operator==(const Expr& e1, const Expr& e2) {
// Comparing pointers (equal expressions are always shared)
return e1.d_expr == e2.d_expr;
}
inline bool operator!=(const Expr& e1, const Expr& e2)
{ return !(e1 == e2); }
// compare() is defined in expr.cpp
inline bool operator<(const Expr& e1, const Expr& e2)
{ return compare(e1,e2) < 0; }
inline bool operator<=(const Expr& e1, const Expr& e2)
{ return compare(e1,e2) <= 0; }
inline bool operator>(const Expr& e1, const Expr& e2)
{ return compare(e1,e2) > 0; }
inline bool operator>=(const Expr& e1, const Expr& e2)
{ return compare(e1,e2) >= 0; }
} // end of namespace CVC3
#endif
syntax highlighted by Code2HTML, v. 0.9.1