#include <theory_quant.h>

Collaboration diagram for CVC3::CompleteInstPreProcessor:

[legend]

List of all members.

Public Member Functions

CompleteInstPreProcessor (TheoryCore *, QuantProofRules *)
bool isGood (const Expr &e)
if e is a formula in the array property fragment
void collectIndex (const Expr &e)
collect index for instantiation
Expr inst (const Expr &e)
inst forall quant using index from collectIndex
bool hasMacros (const std::vector< Expr > &asserts)
if there are macros
Expr instMacros (const Expr &, const Expr)
substitute a macro in assert
Expr simplifyEq (const Expr &)
simplify a=a to True
Expr simplifyQuant (const Expr &)
put all quants in postive form and then skolemize all exists

Private Member Functions

bool isShield (const Expr &e)
if e satisfies the shiled property, that is all bound vars are parameters of uninterpreted functions/predicates and array reads/writes
bool hasShieldVar (const Expr &e)
void addIndex (const Expr &e)
insert an index
void collect_shield_index (const Expr &e)
void collect_forall_index (const Expr &forall_quant)
bool isGoodQuant (const Expr &e)
if e is a quant in the array property fragmenet
Expr plusOne (const Expr &e)
return e+1
Expr minusOne (const Expr &e)
return e-1
void collectHeads (const Expr &assert, std::set< Expr > &heads)
bool isMacro (const Expr &assert)
if assert is a macro definition
Expr recInstMacros (const Expr &assert)
Expr substMacro (const Expr &)
Expr recRewriteNot (const Expr &, ExprMap< Polarity > &)
Expr rewriteNot (const Expr &)
rewrite neg polarity forall / exists to pos polarity
Expr recSkolemize (const Expr &, ExprMap< Polarity > &)
Expr pullVarOut (const Expr &)

Private Attributes

TheoryCore * d_theoryCore
QuantProofRules * d_quant_rules
std::set< Expr > d_allIndex
ExprMap< Polarity > d_expr_pol
ExprMap< Expr > d_quant_equiv_map
std::vector< Expr > d_gnd_cache
ExprMap< bool > d_is_macro_def
ExprMap< Expr > d_macro_quant
ExprMap< Expr > d_macro_def
ExprMap< Expr > d_macro_lhs
bool d_all_good
if all formulas checked so far are good

Detailed Description

Definition at line 97 of file theory_quant.h.

Constructor & Destructor Documentation

CompleteInstPreProcessor::CompleteInstPreProcessor	(	TheoryCore *	core,
		QuantProofRules *	quant_rule
	)

Definition at line 1344 of file theory_quant.cpp.

Member Function Documentation

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 CVC3::Expr::arity(), DebugAssert, CVC3::Expr::getKind(), CVC3::Expr::isBoundVar(), isGround(), isUniterpFunc(), CVC3::READ, and CVC3::WRITE.

Referenced by collect_forall_index(), and isGoodQuant().

bool CompleteInstPreProcessor::hasShieldVar ( const Expr & e ) [private]

Definition at line 1554 of file theory_quant.cpp.

References CVC3::Expr::arity(), CVC3::Expr::getKind(), CVC3::Expr::isBoundVar(), isUniterpFunc(), CVC3::READ, and CVC3::WRITE.

Referenced by isGood().

void CompleteInstPreProcessor::addIndex ( const Expr & e ) [private]

insert an index

Definition at line 1817 of file theory_quant.cpp.

References d_allIndex, d_theoryCore, CVC3::Expr::getType(), CVC3::isInt(), and CVC3::Theory::simplifyExpr().

Referenced by collect_forall_index(), collect_shield_index(), and inst().

void CompleteInstPreProcessor::collect_shield_index ( const Expr & e ) [private]

Definition at line 1832 of file theory_quant.cpp.

References addIndex(), CVC3::Expr::arity(), CVC3::Expr::getKind(), isGround(), isUniterpFunc(), minusOne(), plusOne(), CVC3::READ, and CVC3::WRITE.

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 addIndex(), CVC3::ExprMap< Data >::begin(), collect_shield_index(), DebugAssert, CVC3::ExprMap< Data >::end(), std::endl(), findPolarity(), CVC3::Expr::isBoundVar(), CVC3::Expr::isEq(), isGround(), CVC3::isLE(), CVC3::isLT(), isShield(), MiniSat::left(), minusOne(), CVC3::Neg, plusOne(), CVC3::Pos, CVC3::PosNeg, and MiniSat::right().

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::ExprMap< Data >::begin(), CVC3::Expr::containsBoundVar(), CVC3::ExprMap< Data >::end(), findPolarity(), CVC3::Expr::getVars(), CVC3::Expr::isBoundVar(), CVC3::Expr::isEq(), CVC3::isInt(), CVC3::isLE(), CVC3::isLT(), isShield(), MiniSat::left(), CVC3::Neg, CVC3::Pos, and MiniSat::right().

Referenced by isGood(), and isMacro().

Expr CompleteInstPreProcessor::plusOne ( const Expr & e ) [private]

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_forall_index(), and collect_shield_index().

Expr CompleteInstPreProcessor::minusOne ( const Expr & e ) [private]

return e-1

Definition at line 1827 of file theory_quant.cpp.

References d_theoryCore, CVC3::Theory::getEM(), CVC3::MINUS, and CVC3::ExprManager::newRatExpr().

Referenced by collect_forall_index(), and collect_shield_index().

void CompleteInstPreProcessor::collectHeads	(	const Expr &	assert,
		std::set< Expr > &	heads
	)		`[private]`

Definition at line 1350 of file theory_quant.cpp.

References CVC3::Expr::arity(), CVC3::Expr::getBody(), CVC3::Op::getExpr(), CVC3::Expr::getOp(), CVC3::Expr::getType(), CVC3::Expr::isAbsAtomicFormula(), CVC3::Expr::isAtomicFormula(), CVC3::Type::isBool(), CVC3::Expr::isClosure(), and isUniterpFunc().

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 collectHeads(), CVC3::ExprMap< Data >::count(), d_is_macro_def, d_macro_def, d_macro_lhs, d_macro_quant, d_theoryCore, EXISTS, CVC3::Expr::getBody(), CVC3::Theory::getCommonRules(), CVC3::Theory::getEM(), CVC3::Op::getExpr(), CVC3::Expr::getOp(), CVC3::Expr::getVars(), CVC3::Expr::isForall(), isGoodQuant(), CVC3::Expr::isIff(), isUniterpFunc(), MiniSat::left(), CVC3::ExprManager::newClosureExpr(), MiniSat::right(), and CVC3::CommonProofRules::skolemize().

Referenced by hasMacros(), and instMacros().

Expr CompleteInstPreProcessor::recInstMacros ( const Expr & assert ) [private]

Expr CompleteInstPreProcessor::substMacro ( const Expr & old ) [private]

Definition at line 1432 of file theory_quant.cpp.

References CVC3::ExprMap< Data >::count(), d_macro_def, d_macro_lhs, d_macro_quant, DebugAssert, CVC3::Op::getExpr(), CVC3::Expr::getOp(), 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::arity(), d_theoryCore, DebugAssert, CVC3::ExprMap< Data >::end(), EXISTS, CVC3::ExprMap< Data >::find(), FORALL, CVC3::Theory::getEM(), CVC3::Expr::getOp(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::isClosure(), CVC3::Expr::isForall(), isGround(), CVC3::Expr::isNot(), CVC3::Neg, CVC3::ExprManager::newClosureExpr(), and CVC3::Expr::notExpr().

Referenced by rewriteNot().

Expr CompleteInstPreProcessor::rewriteNot ( const Expr & e ) [private]

rewrite neg polarity forall / exists to pos polarity

Definition at line 1756 of file theory_quant.cpp.

References findPolarity(), getBoundVars(), CVC3::Pos, and recRewriteNot().

Referenced by simplifyQuant().

Expr CompleteInstPreProcessor::recSkolemize	(	const Expr &	e,
		ExprMap< Polarity > &	pol_map
	)		`[private]`

Expr CompleteInstPreProcessor::pullVarOut ( const Expr & thm_expr ) [private]

Definition at line 1249 of file theory_quant.cpp.

References CVC3::Expr::andExpr(), d_theoryCore, EXISTS, FORALL, CVC3::Expr::getBody(), CVC3::Theory::getEM(), CVC3::Expr::getVars(), CVC3::Expr::impExpr(), CVC3::Expr::isAnd(), CVC3::Expr::isExists(), CVC3::Expr::isForall(), CVC3::Expr::isImpl(), CVC3::Expr::isNot(), CVC3::ExprManager::newClosureExpr(), CVC3::Expr::notExpr(), and CVC3::orExpr().

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 CVC3::ExprMap< Data >::begin(), d_all_good, DebugAssert, CVC3::ExprMap< Data >::end(), findPolarityAtomic(), getBoundVars(), hasShieldVar(), CVC3::Expr::isExists(), CVC3::Expr::isForall(), isGoodQuant(), CVC3::Neg, CVC3::Pos, 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 CVC3::ExprMap< Data >::begin(), collect_forall_index(), collect_shield_index(), CVC3::Expr::containsBoundVar(), d_quant_equiv_map, d_theoryCore, DebugAssert, CVC3::ExprMap< Data >::end(), findPolarityAtomic(), CVC3::Theory::getCommonRules(), CVC3::Expr::isAtomicFormula(), CVC3::Expr::isExists(), CVC3::Expr::isForall(), isGround(), CVC3::Pos, pullVarOut(), and CVC3::CommonProofRules::skolemize().

Referenced by CVC3::TheoryQuant::theoryPreprocess().

Expr CompleteInstPreProcessor::inst ( const Expr & e )

inst forall quant using index from collectIndex

Definition at line 2229 of file theory_quant.cpp.

References addIndex(), AND, CVC3::Expr::arity(), CVC3::ExprMap< Data >::count(), d_allIndex, d_quant_equiv_map, d_theoryCore, DebugAssert, CVC3::Expr::getBody(), CVC3::Theory::getEM(), CVC3::Expr::getOp(), recCompleteInster::inst(), CVC3::Expr::isExists(), CVC3::Expr::isForall(), isGround(), CVC3::ExprManager::newRatExpr(), CVC3::Expr::substExpr(), and CVC3::Theory::trueExpr().

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().

Expr CompleteInstPreProcessor::instMacros	(	const Expr &	assert,
		const Expr	macro_quant_sub
	)

substitute a macro in assert

Definition at line 1544 of file theory_quant.cpp.

References isMacro(), and recInstMacros().

Referenced by CVC3::TheoryQuant::theoryPreprocess().

Expr CompleteInstPreProcessor::simplifyEq ( const Expr & assert )

simplify a=a to True

Definition at line 1462 of file theory_quant.cpp.

References CVC3::Expr::arity(), d_theoryCore, DebugAssert, std::endl(), EXISTS, FORALL, CVC3::Expr::getBody(), CVC3::Theory::getEM(), CVC3::Expr::getOp(), CVC3::Expr::getType(), CVC3::Expr::getVars(), CVC3::Expr::isAbsAtomicFormula(), CVC3::Expr::isAtomicFormula(), CVC3::Type::isBool(), CVC3::Expr::isClosure(), CVC3::Expr::isEq(), CVC3::Expr::isExists(), CVC3::Expr::isForall(), CVC3::ExprManager::newClosureExpr(), and CVC3::Theory::trueExpr().

Referenced by CVC3::TheoryQuant::theoryPreprocess().

Expr CompleteInstPreProcessor::simplifyQuant ( const Expr & e )

put all quants in postive form and then skolemize all exists

Definition at line 1731 of file theory_quant.cpp.

References CVC3::CommonProofRules::assumpRule(), d_quant_rules, d_theoryCore, findPolarity(), CVC3::Theory::getCommonRules(), CVC3::Theorem::getExpr(), CVC3::Expr::isForall(), CVC3::QuantProofRules::packVar(), CVC3::Pos, recSkolemize(), rewriteNot(), and TRACE.

Referenced by CVC3::TheoryQuant::theoryPreprocess().

Member Data Documentation

TheoryCore* CVC3::CompleteInstPreProcessor::d_theoryCore [private]

Definition at line 99 of file theory_quant.h.

Referenced by addIndex(), collectIndex(), inst(), isMacro(), minusOne(), plusOne(), pullVarOut(), recInstMacros(), recRewriteNot(), recSkolemize(), simplifyEq(), and simplifyQuant().

QuantProofRules* CVC3::CompleteInstPreProcessor::d_quant_rules [private]

Definition at line 100 of file theory_quant.h.

Referenced by simplifyQuant().

std::set<Expr> CVC3::CompleteInstPreProcessor::d_allIndex [private]

Definition at line 102 of file theory_quant.h.

Referenced by addIndex(), and inst().

ExprMap<Polarity> CVC3::CompleteInstPreProcessor::d_expr_pol [private]

Definition at line 104 of file theory_quant.h.

ExprMap<Expr> CVC3::CompleteInstPreProcessor::d_quant_equiv_map [private]

Definition at line 106 of file theory_quant.h.

Referenced by collectIndex(), and inst().

std::vector<Expr> CVC3::CompleteInstPreProcessor::d_gnd_cache [private]

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().

ExprMap<Expr> CVC3::CompleteInstPreProcessor::d_macro_quant [private]

Definition at line 112 of file theory_quant.h.

Referenced by isMacro(), and substMacro().

ExprMap<Expr> CVC3::CompleteInstPreProcessor::d_macro_def [private]

Definition at line 114 of file theory_quant.h.

Referenced by isMacro(), recInstMacros(), and substMacro().

ExprMap<Expr> CVC3::CompleteInstPreProcessor::d_macro_lhs [private]

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().

The documentation for this class was generated from the following files:

CVC3::CompleteInstPreProcessor Class Reference

Public Member Functions

Private Member Functions

Private Attributes

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation

Member Data Documentation