CVC3
2.4.1
|
#include <cnf_manager.h>
Classes | |
class | CNFCallback |
Abstract class for callbacks. More... | |
struct | Varinfo |
Information kept for each CNF variable. More... |
Public Member Functions | |
CNF_Manager (CVC3::TheoremManager *tm, CVC3::Statistics &statistics, const CVC3::CLFlags &flags) | |
~CNF_Manager () | |
void | registerCNFCallback (CNFCallback *cnfCallback) |
Register CNF callback. | |
void | setBottomScope (int scope) |
Set scope for translation. | |
unsigned | numVars () |
Return the number of variables being managed. | |
unsigned | numFanins (Var c) |
Return number of fanins for CNF node c. | |
Lit | getFanin (Var c, unsigned i) |
Returns the ith fanin of c. | |
unsigned | numFanouts (Var c) |
Return number of fanins for c. | |
Lit | getFanout (Var c, unsigned i) |
Returns the ith fanout of c. | |
const CVC3::Expr & | concreteVar (Var v) |
Convert a CNF literal to an Expr literal. | |
CVC3::Expr | concreteLit (Lit l, bool checkTranslated=true) |
Convert a CNF literal to an Expr literal. | |
Lit | getCNFLit (const CVC3::Expr &e) |
Look up the CNF literal for an Expr. | |
void | cons (unsigned lb, unsigned ub, const CVC3::Expr &e2, std::vector< unsigned > &newLits) |
void | convertLemma (const CVC3::Theorem &thm, CNF_Formula &cnf) |
Convert thm A |- B (A is a set of literals) into one or more clauses. | |
Lit | addAssumption (const CVC3::Theorem &thm, CNF_Formula &cnf) |
Given thm of form A |- B, convert B to CNF and add it to cnf. | |
Lit | addLemma (CVC3::Theorem thm, CNF_Formula &cnf) |
Convert thm to CNF and add it to the current formula. |
Private Member Functions | |
CVC3::CNF_Rules * | createProofRules (CVC3::TheoremManager *tm, const CVC3::CLFlags &) |
void | registerAtom (const CVC3::Expr &e, const CVC3::Theorem &thm) |
Register a new atomic formula. | |
CVC3::Expr | concreteExpr (const CVC3::Expr &e, const Lit &literal) |
Return the expr corresponding to the literal unless the expr is TRUE of FALSE. | |
CVC3::Theorem | concreteThm (const CVC3::Expr &e) |
Return the theorem if e is not as concreteExpr(e). | |
Lit | translateExprRec (const CVC3::Expr &e, CNF_Formula &cnf, const CVC3::Theorem &thmIn) |
Recursively translate e into cnf. | |
CVC3::Theorem | replaceITErec (const CVC3::Expr &e, Var v, bool translateOnly) |
Recursively traverse an expression with an embedded term ITE. | |
Lit | translateExpr (const CVC3::Theorem &thmIn, CNF_Formula &cnf) |
Recursively translate e into cnf. |
Private Attributes | |
CVC3::ValidityChecker * | d_vc |
For clause minimization. | |
bool | d_minimizeClauses |
Whether to use brute-force clause minimization. | |
CVC3::CommonProofRules * | d_commonRules |
Common proof rules. | |
CVC3::CNF_Rules * | d_rules |
Rules for manipulating CNF. | |
std::vector< Varinfo > | d_varInfo |
vector that maps a variable index to information for that variable | |
CVC3::ExprHashMap< Var > | d_cnfVars |
Map from Exprs to Vars representing those Exprs. | |
CVC3::ExprHashMap< CVC3::Theorem > | d_iteMap |
Cached translation of term-ite-containing expressions. | |
int | d_clauseIdNext |
Map of possibly useful lemmas. | |
int | d_bottomScope |
Whether expr has already been translated. | |
std::deque< CVC3::Theorem > | d_translateQueueThms |
Queue of theorems to translate. | |
std::deque< Var > | d_translateQueueVars |
Queue of fanouts corresponding to thms to translate. | |
std::deque< bool > | d_translateQueueFlags |
Whether thm to translate is "translate only". | |
CVC3::Statistics & | d_statistics |
Reference to statistics object. | |
const CVC3::CLFlags & | d_flags |
Reference to command-line flags. | |
const CVC3::Expr & | d_nullExpr |
Reference to null Expr. | |
CNFCallback * | d_cnfCallback |
Instance of CNF_CallBack: must be registered. |
Definition at line 41 of file cnf_manager.h.
CNF_Manager::CNF_Manager | ( | CVC3::TheoremManager * | tm, |
CVC3::Statistics & | statistics, | ||
const CVC3::CLFlags & | flags | ||
) |
Definition at line 35 of file cnf_manager.cpp.
References createProofRules(), d_rules, d_varInfo, d_vc, and CVC3::CLFlags::setFlag().
CNF_Manager::~CNF_Manager | ( | ) |
Definition at line 60 of file cnf_manager.cpp.
|
private |
Definition at line 38 of file cnf_theorem_producer.cpp.
Referenced by CNF_Manager().
|
private |
Register a new atomic formula.
Definition at line 67 of file cnf_manager.cpp.
References d_cnfCallback, DebugAssert, CVC3::Expr::isRegisteredAtom(), CVC3::Expr::isUserRegisteredAtom(), and SAT::CNF_Manager::CNFCallback::registerAtom().
Referenced by translateExprRec().
|
private |
Return the expr corresponding to the literal unless the expr is TRUE of FALSE.
Definition at line 131 of file cnf_manager.cpp.
References concreteLit(), CVC3::Expr::isFalse(), CVC3::Expr::isNot(), and CVC3::Expr::isTrue().
Referenced by translateExprRec().
|
private |
Return the theorem if e is not as concreteExpr(e).
Definition at line 139 of file cnf_manager.cpp.
References d_commonRules, d_iteMap, CVC3::Theorem::isNull(), and CVC3::CommonProofRules::reflexivityRule().
Referenced by translateExprRec().
|
private |
Recursively translate e into cnf.
A non-context dependent cache, d_cnfVars is used to remember translations of expressions. A context-dependent attribute, isTranslated, is used to remember whether an expression has been translated in the current context
Definition at line 147 of file cnf_manager.cpp.
References SAT::CNF_Formula::addLiteral(), AND, CVC3::Expr::begin(), CVC3::CNF_Rules::CNFITEtranslate(), CVC3::CNF_Rules::CNFtranslate(), concreteExpr(), concreteThm(), d_bottomScope, d_cnfVars, d_commonRules, d_flags, d_iteMap, d_rules, d_translateQueueThms, d_translateQueueVars, d_varInfo, DebugAssert, CVC3::ExprHashMap< Data >::end(), CVC3::Expr::end(), CVC3::ExprHashMap< Data >::find(), getCNFLit(), SAT::CNF_Formula::getCurrentClause(), SAT::Lit::getFalse(), CVC3::Expr::getKind(), CVC3::Theorem::getRHS(), SAT::Lit::getTrue(), SAT::Lit::getVar(), IFF, CVC3::Expr::iffExpr(), CVC3::Expr::impExpr(), IMPLIES, CVC3::Expr::isAbsAtomicFormula(), CVC3::Expr::isEq(), CVC3::Expr::isFalse(), CVC3::Expr::isNot(), SAT::Lit::isNull(), CVC3::Theorem::isNull(), CVC3::Expr::isTranslated(), CVC3::Expr::isTrue(), SAT::Lit::isVar(), ITE, MiniSat::left(), SAT::CNF_Formula::newClause(), OR, CVC3::CommonProofRules::reflexivityRule(), registerAtom(), replaceITErec(), MiniSat::right(), SAT::Clause::setClauseTheorem(), CVC3::Expr::setTranslated(), XOR, and CVC3::Expr::xorExpr().
Referenced by addAssumption(), and translateExpr().
|
private |
Recursively traverse an expression with an embedded term ITE.
Term ITE's are handled by introducing a skolem variable for the ITE term and then adding new constraints describing the ITE in terms of the new variable.
Definition at line 74 of file cnf_manager.cpp.
References CVC3::Expr::begin(), d_commonRules, d_iteMap, d_rules, d_translateQueueFlags, d_translateQueueThms, d_translateQueueVars, DebugAssert, CVC3::ExprHashMap< Data >::end(), CVC3::Expr::end(), CVC3::ExprHashMap< Data >::find(), CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), CVC3::Expr::getType(), CVC3::CommonProofRules::iffMP(), CVC3::CNF_Rules::ifLiftRule(), CVC3::Expr::isAtomic(), CVC3::Type::isBool(), CVC3::Theorem::isRefl(), ITE, CVC3::CommonProofRules::reflexivityRule(), CVC3::CommonProofRules::substitutivityRule(), CVC3::CommonProofRules::symmetryRule(), and CVC3::CommonProofRules::varIntroSkolem().
Referenced by translateExprRec().
|
private |
Recursively translate e into cnf.
Call translateExprRec. If additional expressions are queued up, translate them too, until none are left.
Definition at line 510 of file cnf_manager.cpp.
References SAT::CNF_Formula::addLiteral(), CVC3::CNF_Rules::CNFAddUnit(), d_rules, d_translateQueueFlags, d_translateQueueThms, d_translateQueueVars, d_varInfo, SAT::CNF_Formula::getCurrentClause(), CVC3::Theorem::getExpr(), SAT::Lit::getVar(), SAT::CNF_Formula::newClause(), SAT::CNF_Formula::registerUnit(), SAT::Clause::setClauseTheorem(), and translateExprRec().
Referenced by addAssumption(), and addLemma().
|
inline |
Register CNF callback.
Definition at line 166 of file cnf_manager.h.
References d_cnfCallback.
Referenced by CVC3::SearchSat::SearchSat().
|
inline |
|
inline |
Return the number of variables being managed.
Definition at line 173 of file cnf_manager.h.
References d_varInfo.
Referenced by CVC3::SearchSat::newUserAssumptionInt().
|
inline |
Return number of fanins for CNF node c.
A CNF node x is a fanin of CNF node y if the expr for x is a child of the expr for y or if y is an ITE leaf and x is a new CNF node obtained by translating the ITE leaf y.
Definition at line 181 of file cnf_manager.h.
References d_varInfo, and SAT::Var::isVar().
Referenced by getFanin().
Returns the ith fanin of c.
Definition at line 188 of file cnf_manager.h.
References d_varInfo, DebugAssert, and numFanins().
|
inline |
Return number of fanins for c.
x is a fanout of y if y is a fanin of x
Definition at line 197 of file cnf_manager.h.
References d_varInfo, and SAT::Var::isVar().
Referenced by getFanout().
Returns the ith fanout of c.
Definition at line 204 of file cnf_manager.h.
References d_varInfo, DebugAssert, and numFanouts().
|
inline |
Convert a CNF literal to an Expr literal.
Returns a NULL Expr if there is no corresponding Expr for l
Definition at line 212 of file cnf_manager.h.
References d_nullExpr, d_varInfo, and SAT::Var::isNull().
|
inline |
Convert a CNF literal to an Expr literal.
Returns a NULL Expr if there is no corresponding Expr for l
Definition at line 223 of file cnf_manager.h.
References d_nullExpr, d_varInfo, SAT::Lit::getVar(), SAT::Lit::isNull(), and SAT::Lit::isPositive().
Referenced by CVC3::SearchSat::checkJustified(), concreteExpr(), generateSatProof(), and CVC3::SearchSat::setJustified().
|
inline |
Look up the CNF literal for an Expr.
Returns a NULL Lit if there is no corresponding CNF literal for e
Definition at line 236 of file cnf_manager.h.
References d_cnfVars, CVC3::ExprHashMap< Data >::end(), CVC3::ExprHashMap< Data >::find(), SAT::Lit::getFalse(), SAT::Lit::getTrue(), CVC3::Expr::isFalse(), CVC3::Expr::isNot(), CVC3::Expr::isTranslated(), and CVC3::Expr::isTrue().
Referenced by convertLemma(), CVC3::SearchSat::getValue(), and translateExprRec().
void CNF_Manager::cons | ( | unsigned | lb, |
unsigned | ub, | ||
const CVC3::Expr & | e2, | ||
std::vector< unsigned > & | newLits | ||
) |
Definition at line 550 of file cnf_manager.cpp.
References CVC3::ValidityChecker::assertFormula(), d_vc, CVC3::ValidityChecker::falseExpr(), CVC3::ValidityChecker::pop(), CVC3::ValidityChecker::push(), CVC3::ValidityChecker::query(), and CVC3::VALID.
void CNF_Manager::convertLemma | ( | const CVC3::Theorem & | thm, |
CNF_Formula & | cnf | ||
) |
Convert thm A |- B (A is a set of literals) into one or more clauses.
cnf should be empty – it will be filled with the result
Definition at line 593 of file cnf_manager.cpp.
References SAT::CNF_Formula::addLiteral(), CVC3::Expr::begin(), CVC3::CNF_Rules::CNFAddUnit(), CVC3::CNF_Rules::CNFConvert(), d_rules, DebugAssert, SAT::CNF_Formula::empty(), CVC3::Expr::end(), getCNFLit(), SAT::CNF_Formula::getCurrentClause(), SAT::Lit::isNull(), CVC3::Expr::isOr(), CVC3::CNF_Rules::learnedClauses(), SAT::CNF_Formula::newClause(), SAT::CNF_Formula::registerUnit(), and SAT::Clause::setClauseTheorem().
Lit CNF_Manager::addAssumption | ( | const CVC3::Theorem & | thm, |
CNF_Formula & | cnf | ||
) |
Given thm of form A |- B, convert B to CNF and add it to cnf.
Returns Lit corresponding to the root of the expression that was translated.
Definition at line 623 of file cnf_manager.cpp.
References SAT::CNF_Formula::addLiteral(), CVC3::Expr::arity(), CVC3::CNF_Rules::CNFAddUnit(), d_flags, d_rules, DebugAssert, SAT::CNF_Formula::getCurrentClause(), CVC3::Theorem::getExpr(), CVC3::Expr::isFalse(), CVC3::Expr::isNot(), CVC3::Expr::isOr(), CVC3::Expr::isTrue(), SAT::CNF_Formula::newClause(), SAT::CNF_Formula::registerUnit(), SAT::Clause::setClauseTheorem(), CVC3::Expr::toString(), translateExpr(), and translateExprRec().
Referenced by CVC3::SearchSat::newUserAssumptionIntHelper().
Lit CNF_Manager::addLemma | ( | CVC3::Theorem | thm, |
CNF_Formula & | cnf | ||
) |
Convert thm to CNF and add it to the current formula.
thm | should be of form A |- B where A is a set of literals. |
cnf | the new clauses are added to cnf. Returns Lit corresponding to the root of the expression that was translated. |
Definition at line 674 of file cnf_manager.cpp.
References SAT::CNF_Formula::addLiteral(), CVC3::CNF_Rules::CNFAddUnit(), d_rules, DebugAssert, SAT::CNF_Formula::getCurrentClause(), CVC3::CNF_Rules::learnedClauses(), SAT::CNF_Formula::newClause(), SAT::CNF_Formula::registerUnit(), SAT::Clause::setClauseTheorem(), and translateExpr().
|
private |
For clause minimization.
Definition at line 44 of file cnf_manager.h.
Referenced by CNF_Manager(), cons(), and ~CNF_Manager().
|
private |
Whether to use brute-force clause minimization.
Definition at line 47 of file cnf_manager.h.
|
private |
Common proof rules.
Definition at line 50 of file cnf_manager.h.
Referenced by concreteThm(), replaceITErec(), and translateExprRec().
|
private |
Rules for manipulating CNF.
Definition at line 53 of file cnf_manager.h.
Referenced by addAssumption(), addLemma(), CNF_Manager(), convertLemma(), replaceITErec(), translateExpr(), translateExprRec(), and ~CNF_Manager().
|
private |
vector that maps a variable index to information for that variable
Definition at line 63 of file cnf_manager.h.
Referenced by CNF_Manager(), concreteLit(), concreteVar(), getFanin(), getFanout(), numFanins(), numFanouts(), numVars(), translateExpr(), and translateExprRec().
|
private |
Map from Exprs to Vars representing those Exprs.
Definition at line 66 of file cnf_manager.h.
Referenced by getCNFLit(), and translateExprRec().
|
private |
Cached translation of term-ite-containing expressions.
Definition at line 69 of file cnf_manager.h.
Referenced by concreteThm(), replaceITErec(), and translateExprRec().
|
private |
Map of possibly useful lemmas.
Maps a clause id to the theorem justifying that clause
Note that clauses created by simple CNF translation are not given id's. This is because theorems for these clauses can be created lazily later. Next clause id
Definition at line 81 of file cnf_manager.h.
|
private |
Whether expr has already been translated.
Bottom scope in which translation is valid
Definition at line 87 of file cnf_manager.h.
Referenced by setBottomScope(), and translateExprRec().
|
private |
Queue of theorems to translate.
Definition at line 90 of file cnf_manager.h.
Referenced by replaceITErec(), translateExpr(), and translateExprRec().
|
private |
Queue of fanouts corresponding to thms to translate.
Definition at line 93 of file cnf_manager.h.
Referenced by replaceITErec(), translateExpr(), and translateExprRec().
|
private |
Whether thm to translate is "translate only".
Definition at line 96 of file cnf_manager.h.
Referenced by replaceITErec(), and translateExpr().
|
private |
Reference to statistics object.
Definition at line 99 of file cnf_manager.h.
|
private |
Reference to command-line flags.
Definition at line 102 of file cnf_manager.h.
Referenced by addAssumption(), and translateExprRec().
|
private |
Reference to null Expr.
Definition at line 105 of file cnf_manager.h.
Referenced by concreteLit(), and concreteVar().
|
private |
Instance of CNF_CallBack: must be registered.
Definition at line 120 of file cnf_manager.h.
Referenced by registerAtom(), and registerCNFCallback().