35 #ifndef _cvc3__expr_h_
39 #ifndef _cvc3__assumptions_h_
40 #define _cvc3__assumptions_h_
59 std::vector<Theorem>& gamma);
61 std::vector<Theorem>& gamma);
63 void add(
const std::vector<Theorem>& thms);
118 class iterator :
public std::iterator<std::input_iterator_tag,Theorem,ptrdiff_t> {
122 std::vector<Theorem>::const_iterator
d_it;
161 const std::vector<Expr>& es);
163 friend std::ostream&
operator<<(std::ostream& os,
Assumptions()
Default constructor: no value is created.
iterator(const std::vector< Theorem >::const_iterator &i)
iterator & operator++()
Prefix increment.
friend std::ostream & operator<<(std::ostream &os, const Assumptions &assump)
const Theorem & find(const Expr &e) const
static bool findExprs(const Assumptions &a, const std::vector< Expr > &es, std::vector< Theorem > &gamma)
Data structure of expressions in CVC3.
friend Assumptions operator-(const Assumptions &a, const Expr &e)
Returns all (recursive) assumptions except e.
iterator()
Default constructor.
void add(const std::vector< Theorem > &thms)
static Assumptions s_empty
Assumptions(const Assumptions &assump)
const Theorem & findTheorem(const Expr &e) const
const Theorem & operator[](const Expr &e) const
const Theorem & operator*() const
Dereference operator.
#define DebugAssert(cond, str)
Proxy operator++(int)
Postfix increment.
Assumptions & operator=(const Assumptions &assump)
bool operator!=(const iterator &i) const
Disequality.
bool operator==(const iterator &i) const
Equality.
const Theorem * operator->() const
Member dereference operator.
Assumptions(const Theorem &t)
Constructor for one theorem (common case)
Proxy class for postfix increment.
friend bool operator!=(const Assumptions &a1, const Assumptions &a2)
friend bool operator==(const Assumptions &a1, const Assumptions &a2)
std::vector< Theorem > d_vector
const Theorem & operator*()
Definition of the API to expression package. See class Expr for details.
void add1(const Theorem &t)
Iterator for the Assumptions: points to class Theorem.
std::vector< Theorem >::const_iterator d_it
void add(const Assumptions &a)
std::string toString() const
static const Assumptions & emptyAssump()
static bool findExpr(const Assumptions &a, const Expr &e, std::vector< Theorem > &gamma)