32 for (
int i = 0; i < e.
arity(); i++)
44 #define vals3(a, b, c) ((a) + 1 + ((b) + 1) * 3 + ((c) + 1) * 9)
45 #define vals4(a, b, c, d) (vals3(a, b, c) + ((d) + 1) * 27)
159 case vals4(-1,-1,1,-1):
case vals4(-1,-1,-1,-1):
193 case vals4(-1,-1,-1,1):
virtual Theorem confAndrAT(const Theorem &andr_th, const Theorem &a_th, bool left, const Theorem &b_th)=0
Data structure of expressions in CVC3.
virtual Theorem confIterThenElse(const Theorem &iter_th, const Theorem &ite_th, const Theorem &then_th, const Theorem &else_th)=0
virtual Theorem propAndrAT(const Theorem &andr_th, const Theorem &l_th, const Theorem &r_th)=0
ExprHashMap< std::vector< Circuit * > > d_circuitsByExpr
virtual void propIterIfThen(const Theorem &iter_th, bool left, const Theorem &ite_th, const Theorem &then_th, Theorem *if_th, Theorem *else_th)=0
StatCounter d_circuitPropCount
Total number of circuit propagations.
void recordFact(const Theorem &thm)
Process a new derived fact (auxiliary function)
Literal newLiteral(const Expr &e)
Construct a Literal out of an Expr or return an existing one.
Theorem d_conflictTheorem
Theorem(FALSE) which generated a conflict.
#define DebugAssert(cond, str)
VariableManager * d_vm
Variable manager for classes Variable and Literal.
virtual Theorem propIterIte(const Theorem &iter_th, bool left, const Theorem &if_th, const Theorem &then_th)=0
SearchEngineRules * d_rules
Proof rules for the search engine.
Abstract proof rules interface to the simple search engine.
std::vector< Literal > d_literals
Set of literals to be processed by bcp.
virtual void propAndrLRT(const Theorem &andr_th, const Theorem &a_th, Theorem *l_th, Theorem *r_th)=0
virtual Theorem propAndrRF(const Theorem &andr_th, const Theorem &a_th, const Theorem &l_th)=0
const Theorem & getTheorem() const
Implementation of a faster search engine, using newer techniques.
virtual Theorem confIffr(const Theorem &iffr_th, const Theorem &i_th, const Theorem &l_th, const Theorem &r_th)=0
virtual Theorem confAndrAF(const Theorem &andr_th, const Theorem &a_th, const Theorem &l_th, const Theorem &r_th)=0
#define vals4(a, b, c, d)
virtual Theorem propIffr(const Theorem &iffr_th, int p, const Theorem &a_th, const Theorem &b_th)=0
virtual Theorem confIterIfThen(const Theorem &iter_th, bool left, const Theorem &ite_th, const Theorem &if_th, const Theorem &then_th)=0
virtual Theorem propAndrLF(const Theorem &andr_th, const Theorem &a_th, const Theorem &r_th)=0
void addFact(const Theorem &e)
Add a new assertion to the core from the user or a SAT solver. Do NOT use it in a decision procedure;...
bool propagate(SearchEngineFast *se)
TheoryCore * d_core
Access to theory reasoning.
virtual Theorem propAndrAF(const Theorem &andr_th, bool left, const Theorem &b_th)=0
virtual Theorem propIterThen(const Theorem &iter_th, const Theorem &ite_th, const Theorem &if_th)=0