CVC3
2.4.1
|
#include <theory_quant.h>
CompleteInstPreProcessor::CompleteInstPreProcessor | ( | TheoryCore * | core, |
QuantProofRules * | quant_rule | ||
) |
Definition at line 1344 of file theory_quant.cpp.
bool CompleteInstPreProcessor::isShield | ( | const Expr & | e | ) | [private] |
if e satisfies the shiled property, that is all bound vars are parameters of uninterpreted functions/predicates and array reads/writes
Definition at line 1577 of file theory_quant.cpp.
References isGround(), isUniterpFunc(), CVC3::Expr::arity(), CVC3::Expr::isBoundVar(), CVC3::Expr::getKind(), CVC3::READ, CVC3::WRITE, and DebugAssert.
Referenced by collect_forall_index(), and isGoodQuant().
bool CompleteInstPreProcessor::hasShieldVar | ( | const Expr & | e | ) | [private] |
Definition at line 1554 of file theory_quant.cpp.
References isUniterpFunc(), CVC3::Expr::arity(), CVC3::Expr::getKind(), CVC3::READ, CVC3::WRITE, and CVC3::Expr::isBoundVar().
Referenced by isGood().
void CompleteInstPreProcessor::addIndex | ( | const Expr & | e | ) | [private] |
insert an index
Definition at line 1817 of file theory_quant.cpp.
References CVC3::isInt(), CVC3::Expr::getType(), d_allIndex, d_theoryCore, and CVC3::Theory::simplifyExpr().
Referenced by collect_shield_index(), collect_forall_index(), and inst().
void CompleteInstPreProcessor::collect_shield_index | ( | const Expr & | e | ) | [private] |
Definition at line 1832 of file theory_quant.cpp.
References isUniterpFunc(), CVC3::Expr::arity(), isGround(), addIndex(), CVC3::Expr::getKind(), CVC3::READ, CVC3::WRITE, plusOne(), and minusOne().
Referenced by collect_forall_index(), and collectIndex().
void CompleteInstPreProcessor::collect_forall_index | ( | const Expr & | forall_quant | ) | [private] |
Definition at line 1861 of file theory_quant.cpp.
References findPolarity(), CVC3::Pos, CVC3::ExprMap::begin(), CVC3::ExprMap::end(), CVC3::isLE(), MiniSat::left(), MiniSat::right(), CVC3::Expr::isBoundVar(), isGround(), CVC3::PosNeg, addIndex(), plusOne(), CVC3::Neg, isShield(), collect_shield_index(), std::endl(), DebugAssert, CVC3::Expr::isEq(), minusOne(), and CVC3::isLT().
Referenced by collectIndex().
bool CompleteInstPreProcessor::isGoodQuant | ( | const Expr & | e | ) | [private] |
if e is a quant in the array property fragmenet
Definition at line 2103 of file theory_quant.cpp.
References CVC3::Expr::getVars(), CVC3::isInt(), findPolarity(), CVC3::Pos, CVC3::ExprMap::begin(), CVC3::ExprMap::end(), CVC3::Expr::containsBoundVar(), isShield(), CVC3::isLE(), CVC3::isLT(), CVC3::Expr::isEq(), MiniSat::left(), MiniSat::right(), CVC3::Expr::isBoundVar(), and CVC3::Neg.
return e+1
Definition at line 1822 of file theory_quant.cpp.
References d_theoryCore, CVC3::Theory::getEM(), CVC3::ExprManager::newRatExpr(), and CVC3::PLUS.
Referenced by collect_shield_index(), and collect_forall_index().
return e-1
Definition at line 1827 of file theory_quant.cpp.
References d_theoryCore, CVC3::Theory::getEM(), CVC3::ExprManager::newRatExpr(), and CVC3::MINUS.
Referenced by collect_shield_index(), and collect_forall_index().
void CompleteInstPreProcessor::collectHeads | ( | const Expr & | assert, |
std::set< Expr > & | heads | ||
) | [private] |
Definition at line 1350 of file theory_quant.cpp.
References CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::isAbsAtomicFormula(), CVC3::Expr::arity(), CVC3::Expr::isClosure(), CVC3::Expr::getBody(), CVC3::Expr::isAtomicFormula(), isUniterpFunc(), CVC3::Expr::getOp(), and CVC3::Op::getExpr().
Referenced by isMacro().
bool CompleteInstPreProcessor::isMacro | ( | const Expr & | assert | ) | [private] |
if assert is a macro definition
Definition at line 1373 of file theory_quant.cpp.
References d_is_macro_def, CVC3::ExprMap::count(), CVC3::Expr::isForall(), CVC3::Expr::getBody(), CVC3::Expr::isIff(), MiniSat::right(), MiniSat::left(), isUniterpFunc(), d_theoryCore, CVC3::Theory::getEM(), CVC3::ExprManager::newClosureExpr(), EXISTS, CVC3::Expr::getVars(), CVC3::Theory::getCommonRules(), CVC3::CommonProofRules::skolemize(), isGoodQuant(), CVC3::Expr::getOp(), CVC3::Op::getExpr(), collectHeads(), d_macro_quant, d_macro_def, and d_macro_lhs.
Referenced by hasMacros(), and instMacros().
Definition at line 1499 of file theory_quant.cpp.
References CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::isAbsAtomicFormula(), CVC3::Expr::arity(), CVC3::Expr::getOp(), CVC3::Expr::isClosure(), CVC3::Expr::getBody(), CVC3::Expr::isForall(), d_theoryCore, CVC3::Theory::getEM(), CVC3::ExprManager::newClosureExpr(), FORALL, CVC3::Expr::getVars(), CVC3::Expr::isExists(), EXISTS, DebugAssert, CVC3::Expr::isAtomicFormula(), isUniterpFunc(), CVC3::Op::getExpr(), d_macro_def, CVC3::ExprMap::count(), and substMacro().
Referenced by instMacros().
Definition at line 1432 of file theory_quant.cpp.
References CVC3::Expr::getOp(), CVC3::Op::getExpr(), DebugAssert, d_macro_lhs, CVC3::ExprMap::count(), d_macro_def, d_macro_quant, CVC3::Expr::getVars(), and CVC3::Expr::substExpr().
Referenced by recInstMacros().
Expr CompleteInstPreProcessor::recRewriteNot | ( | const Expr & | e, |
ExprMap< Polarity > & | pol_map | ||
) | [private] |
Definition at line 1763 of file theory_quant.cpp.
References CVC3::Expr::getType(), CVC3::Type::isBool(), isGround(), CVC3::Expr::isClosure(), DebugAssert, CVC3::ExprMap::find(), CVC3::ExprMap::end(), CVC3::Neg, CVC3::Expr::notExpr(), CVC3::Expr::isForall(), EXISTS, FORALL, d_theoryCore, CVC3::Theory::getEM(), CVC3::ExprManager::newClosureExpr(), CVC3::Expr::arity(), CVC3::Expr::isNot(), and CVC3::Expr::getOp().
Referenced by rewriteNot().
rewrite neg polarity forall / exists to pos polarity
Definition at line 1756 of file theory_quant.cpp.
References findPolarity(), CVC3::Pos, getBoundVars(), and recRewriteNot().
Referenced by simplifyQuant().
Expr CompleteInstPreProcessor::recSkolemize | ( | const Expr & | e, |
ExprMap< Polarity > & | pol_map | ||
) | [private] |
Definition at line 1693 of file theory_quant.cpp.
References CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::isClosure(), CVC3::Expr::isForall(), CVC3::Expr::isExists(), CVC3::Pos, CVC3::Expr::getBody(), d_theoryCore, CVC3::Theory::getEM(), CVC3::ExprManager::newClosureExpr(), EXISTS, CVC3::Expr::getVars(), CVC3::Theory::getCommonRules(), CVC3::CommonProofRules::skolemize(), CVC3::Expr::arity(), CVC3::Expr::isNot(), and CVC3::Expr::getOp().
Referenced by simplifyQuant().
Definition at line 1249 of file theory_quant.cpp.
References CVC3::Expr::getBody(), CVC3::Expr::isForall(), CVC3::Expr::isNot(), CVC3::Expr::isAnd(), CVC3::Expr::isExists(), CVC3::Expr::getVars(), CVC3::Expr::notExpr(), CVC3::orExpr(), d_theoryCore, CVC3::Theory::getEM(), CVC3::ExprManager::newClosureExpr(), FORALL, CVC3::Expr::isImpl(), CVC3::Expr::andExpr(), CVC3::Expr::impExpr(), and EXISTS.
Referenced by collectIndex().
bool CompleteInstPreProcessor::isGood | ( | const Expr & | e | ) |
if e is a formula in the array property fragment
Definition at line 2022 of file theory_quant.cpp.
References getBoundVars(), findPolarityAtomic(), CVC3::Pos, CVC3::ExprMap::begin(), CVC3::ExprMap::end(), CVC3::Expr::isForall(), isGoodQuant(), hasShieldVar(), d_all_good, DebugAssert, CVC3::Expr::isExists(), CVC3::Neg, and CVC3::PosNeg.
Referenced by CVC3::TheoryQuant::theoryPreprocess().
void CompleteInstPreProcessor::collectIndex | ( | const Expr & | e | ) |
collect index for instantiation
Definition at line 1972 of file theory_quant.cpp.
References isGround(), collect_shield_index(), findPolarityAtomic(), CVC3::Pos, CVC3::ExprMap::begin(), CVC3::ExprMap::end(), CVC3::Expr::isAtomicFormula(), CVC3::Expr::containsBoundVar(), DebugAssert, CVC3::Expr::isForall(), pullVarOut(), collect_forall_index(), d_quant_equiv_map, CVC3::Expr::isExists(), d_theoryCore, CVC3::Theory::getCommonRules(), and CVC3::CommonProofRules::skolemize().
Referenced by CVC3::TheoryQuant::theoryPreprocess().
inst forall quant using index from collectIndex
Definition at line 2229 of file theory_quant.cpp.
References isGround(), CVC3::Expr::isExists(), DebugAssert, d_quant_equiv_map, CVC3::ExprMap::count(), CVC3::Expr::isForall(), CVC3::Expr::arity(), CVC3::Expr::getOp(), CVC3::Expr::getBody(), d_allIndex, addIndex(), d_theoryCore, CVC3::Theory::getEM(), CVC3::ExprManager::newRatExpr(), CVC3::Expr::substExpr(), AND, CVC3::Theory::trueExpr(), and recCompleteInster::inst().
Referenced by CVC3::TheoryQuant::theoryPreprocess().
bool CompleteInstPreProcessor::hasMacros | ( | const std::vector< Expr > & | asserts | ) |
if there are macros
Definition at line 1421 of file theory_quant.cpp.
References isMacro().
Referenced by CVC3::TheoryQuant::theoryPreprocess().
substitute a macro in assert
Definition at line 1544 of file theory_quant.cpp.
References isMacro(), and recInstMacros().
Referenced by CVC3::TheoryQuant::theoryPreprocess().
simplify a=a to True
Definition at line 1462 of file theory_quant.cpp.
References CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::isAbsAtomicFormula(), CVC3::Expr::arity(), CVC3::Expr::getOp(), CVC3::Expr::isClosure(), CVC3::Expr::getBody(), CVC3::Expr::isForall(), d_theoryCore, CVC3::Theory::getEM(), CVC3::ExprManager::newClosureExpr(), FORALL, CVC3::Expr::getVars(), CVC3::Expr::isExists(), EXISTS, DebugAssert, CVC3::Expr::isAtomicFormula(), CVC3::Expr::isEq(), CVC3::Theory::trueExpr(), and std::endl().
Referenced by CVC3::TheoryQuant::theoryPreprocess().
put all quants in postive form and then skolemize all exists
Definition at line 1731 of file theory_quant.cpp.
References rewriteNot(), TRACE, CVC3::Expr::isForall(), d_theoryCore, CVC3::Theory::getCommonRules(), CVC3::CommonProofRules::assumpRule(), d_quant_rules, CVC3::QuantProofRules::packVar(), CVC3::Theorem::getExpr(), findPolarity(), CVC3::Pos, and recSkolemize().
Referenced by CVC3::TheoryQuant::theoryPreprocess().
Definition at line 99 of file theory_quant.h.
Referenced by pullVarOut(), isMacro(), simplifyEq(), recInstMacros(), recSkolemize(), simplifyQuant(), recRewriteNot(), addIndex(), plusOne(), minusOne(), collectIndex(), and inst().
Definition at line 100 of file theory_quant.h.
Referenced by simplifyQuant().
Definition at line 102 of file theory_quant.h.
Referenced by addIndex(), and inst().
Definition at line 104 of file theory_quant.h.
Definition at line 106 of file theory_quant.h.
Referenced by collectIndex(), and inst().
Definition at line 108 of file theory_quant.h.
ExprMap<bool> CVC3::CompleteInstPreProcessor::d_is_macro_def [private] |
Definition at line 110 of file theory_quant.h.
Referenced by isMacro().
Definition at line 112 of file theory_quant.h.
Referenced by isMacro(), and substMacro().
Definition at line 114 of file theory_quant.h.
Referenced by isMacro(), substMacro(), and recInstMacros().
Definition at line 116 of file theory_quant.h.
Referenced by isMacro(), and substMacro().
bool CVC3::CompleteInstPreProcessor::d_all_good [private] |
if all formulas checked so far are good
Definition at line 119 of file theory_quant.h.
Referenced by isGood().