21 #ifndef _cvc3__include__cnf_manager_h_
22 #define _cvc3__include__cnf_manager_h_
32 class CommonProofRules;
34 class ValidityChecker;
167 { d_cnfCallback = cnfCallback; }
173 unsigned numVars() {
return d_varInfo.size(); }
182 if (!c.
isVar())
return 0;
183 if (
unsigned(c) >= d_varInfo.size())
return 0;
184 return d_varInfo[c].fanins.size();
190 return d_varInfo[c].fanins[i];
198 if (!c.
isVar())
return 0;
199 if (
unsigned(c) >= d_varInfo.size())
return 0;
200 return d_varInfo[c].fanouts.size();
206 return Lit(d_varInfo[c].fanouts[i]);
213 if (v.
isNull())
return d_nullExpr;
214 if (
unsigned(v) >= d_varInfo.size() ||
215 (!d_varInfo[v].expr.isTranslated()))
217 return d_varInfo[v].expr;
224 if (l.
isNull())
return d_nullExpr;
227 if ((
unsigned)index >= d_varInfo.size() ||
228 (checkTranslated && !d_varInfo[index].expr.isTranslated()))
230 return inverted ? !d_varInfo[index].expr : d_varInfo[index].expr;
242 return Lit((*i).second);
245 void cons(
unsigned lb,
unsigned ub,
const CVC3::Expr& e2, std::vector<unsigned>& newLits);
Basic classes for reasoning about formulas in CNF.
std::deque< bool > d_translateQueueFlags
Whether thm to translate is "translate only".
void registerCNFCallback(CNFCallback *cnfCallback)
Register CNF callback.
Data structure of expressions in CVC3.
unsigned numVars()
Return the number of variables being managed.
std::vector< Varinfo > d_varInfo
vector that maps a variable index to information for that variable
API to the CNF proof rules.
Lit getFanout(Var c, unsigned i)
Returns the ith fanout of c.
Lit translateExpr(const CVC3::Theorem &thmIn, CNF_Formula &cnf)
Recursively translate e into cnf.
bool isTranslated() const
std::deque< CVC3::Theorem > d_translateQueueThms
Queue of theorems to translate.
virtual void registerAtom(const CVC3::Expr &e, const CVC3::Theorem &thm)=0
Register an atom.
Lit translateExprRec(const CVC3::Expr &e, CNF_Formula &cnf, const CVC3::Theorem &thmIn)
Recursively translate e into cnf.
#define DebugAssert(cond, str)
void registerAtom(const CVC3::Expr &e, const CVC3::Theorem &thm)
Register a new atomic formula.
int d_clauseIdNext
Map of possibly useful lemmas.
Lit getCNFLit(const CVC3::Expr &e)
Look up the CNF literal for an Expr.
CVC3::ExprHashMap< CVC3::Theorem > d_iteMap
Cached translation of term-ite-containing expressions.
Description: Counters and flags for collecting run-time statistics.
CVC3::Theorem replaceITErec(const CVC3::Expr &e, Var v, bool translateOnly)
Recursively traverse an expression with an embedded term ITE.
void cons(unsigned lb, unsigned ub, const CVC3::Expr &e2, std::vector< unsigned > &newLits)
Lit getFanin(Var c, unsigned i)
Returns the ith fanin of c.
Information kept for each CNF variable.
CNFCallback * d_cnfCallback
Instance of CNF_CallBack: must be registered.
CVC3::Theorem concreteThm(const CVC3::Expr &e)
Return the theorem if e is not as concreteExpr(e).
unsigned numFanins(Var c)
Return number of fanins for CNF node c.
CVC3::ExprHashMap< Var > d_cnfVars
Map from Exprs to Vars representing those Exprs.
std::deque< Var > d_translateQueueVars
Queue of fanouts corresponding to thms to translate.
CVC3::Statistics & d_statistics
Reference to statistics object.
CVC3::CNF_Rules * createProofRules(CVC3::TheoremManager *tm, const CVC3::CLFlags &)
Generic API for a validity checker.
CVC3::ValidityChecker * d_vc
For clause minimization.
Abstract class for callbacks.
CVC3::CommonProofRules * d_commonRules
Common proof rules.
CVC3::Expr concreteLit(Lit l, bool checkTranslated=true)
Convert a CNF literal to an Expr literal.
unsigned numFanouts(Var c)
Return number of fanins for c.
iterator find(const Expr &e)
bool d_minimizeClauses
Whether to use brute-force clause minimization.
const CVC3::CLFlags & d_flags
Reference to command-line flags.
Definition of the API to expression package. See class Expr for details.
CNF_Manager(CVC3::TheoremManager *tm, CVC3::Statistics &statistics, const CVC3::CLFlags &flags)
std::vector< Lit > fanins
CVC3::Expr concreteExpr(const CVC3::Expr &e, const Lit &literal)
Return the expr corresponding to the literal unless the expr is TRUE of FALSE.
void setBottomScope(int scope)
Set scope for translation.
int d_bottomScope
Whether expr has already been translated.
void convertLemma(const CVC3::Theorem &thm, CNF_Formula &cnf)
Convert thm A |- B (A is a set of literals) into one or more clauses.
const CVC3::Expr & d_nullExpr
Reference to null Expr.
CVC3::CNF_Rules * d_rules
Rules for manipulating CNF.
const CVC3::Expr & concreteVar(Var v)
Convert a CNF literal to an Expr literal.
Lit addAssumption(const CVC3::Theorem &thm, CNF_Formula &cnf)
Given thm of form A |- B, convert B to CNF and add it to cnf.
std::vector< Var > fanouts
Lit addLemma(CVC3::Theorem thm, CNF_Formula &cnf)
Convert thm to CNF and add it to the current formula.