CVC3::CompleteInstPreProcessor Class Reference

#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
  

• 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 *	,
		QuantProofRules *
	)

Definition at line 1337 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 1547 of file theory_quant.cpp.

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

Referenced by collect_forall_index(), and isGoodQuant().

void CompleteInstPreProcessor::addIndex

(

const Expr &

e

)

[private]

insert an index

Definition at line 1787 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 1802 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 1831 of file theory_quant.cpp.

References addIndex(), CVC3::ExprMap< Data >::begin(), collect_shield_index(), DebugAssert, CVC3::ExprMap< Data >::end(), std::endl(), findPolarity(), 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 2070 of file theory_quant.cpp.

References CVC3::ExprMap< Data >::begin(), CVC3::ExprMap< Data >::end(), findPolarity(), CVC3::Expr::getVars(), 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 1792 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 1797 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 1343 of file theory_quant.cpp.

References CVC3::Expr::arity(), CVC3::Expr::getBody(), 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 1366 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, CVC3::EXISTS, CVC3::Expr::getBody(), CVC3::Theory::getCommonRules(), CVC3::Theory::getEM(), CVC3::Op::getExpr(), CVC3::Expr::getOp(), CVC3::Expr::getVars(), CVC3::Expr::isForall(), isGoodQuant(), isUniterpFunc(), MiniSat::left(), CVC3::ExprManager::newClosureExpr(), MiniSat::right(), and CVC3::CommonProofRules::skolemize().

Referenced by hasMacros(), and instMacros().

Expr CompleteInstPreProcessor::recInstMacros

(

const Expr &

assert

)

[private]

Definition at line 1492 of file theory_quant.cpp.

References CVC3::Expr::arity(), CVC3::ExprMap< Data >::count(), d_macro_def, d_theoryCore, DebugAssert, CVC3::EXISTS, CVC3::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::isExists(), CVC3::Expr::isForall(), isUniterpFunc(), CVC3::ExprManager::newClosureExpr(), and substMacro().

Referenced by instMacros().

Expr CompleteInstPreProcessor::substMacro

(

const Expr &

)

[private]

Definition at line 1425 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 &	,
		ExprMap< Polarity > &
	)			[private]

Definition at line 1733 of file theory_quant.cpp.

References d_theoryCore, DebugAssert, CVC3::ExprMap< Data >::end(), CVC3::EXISTS, CVC3::ExprMap< Data >::find(), CVC3::FORALL, CVC3::Theory::getEM(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::isForall(), isGround(), CVC3::Expr::isNot(), CVC3::Neg, CVC3::ExprManager::newClosureExpr(), and CVC3::Expr::notExpr().

Referenced by rewriteNot().

Expr CompleteInstPreProcessor::rewriteNot

(

const Expr &

)

[private]

rewrite neg polarity forall / exists to pos polarity

Definition at line 1726 of file theory_quant.cpp.

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

Referenced by simplifyQuant().

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

Definition at line 1663 of file theory_quant.cpp.

References d_theoryCore, CVC3::EXISTS, CVC3::Theory::getCommonRules(), CVC3::Theory::getEM(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::isClosure(), CVC3::Expr::isNot(), CVC3::ExprManager::newClosureExpr(), CVC3::Pos, and CVC3::CommonProofRules::skolemize().

Referenced by simplifyQuant().

Expr CompleteInstPreProcessor::pullVarOut

(

const Expr &

)

[private]

Definition at line 1242 of file theory_quant.cpp.

References CVC3::andExpr(), d_theoryCore, CVC3::EXISTS, CVC3::FORALL, CVC3::Expr::getBody(), CVC3::Theory::getEM(), CVC3::Expr::getVars(), 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 1992 of file theory_quant.cpp.

References CVC3::ExprMap< Data >::begin(), d_all_good, DebugAssert, CVC3::ExprMap< Data >::end(), findPolarityAtomic(), getBoundVars(), 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 1942 of file theory_quant.cpp.

References CVC3::ExprMap< Data >::begin(), collect_forall_index(), collect_shield_index(), d_quant_equiv_map, d_theoryCore, DebugAssert, CVC3::ExprMap< Data >::end(), findPolarityAtomic(), CVC3::Theory::getCommonRules(), 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 2176 of file theory_quant.cpp.

References addIndex(), CVC3::AND, CVC3::Expr::arity(), CVC3::ExprMap< Data >::count(), d_allIndex, d_quant_equiv_map, d_theoryCore, DebugAssert, 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 1414 of file theory_quant.cpp.

References isMacro().

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

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

substitute a macro in assert

Definition at line 1537 of file theory_quant.cpp.

References isMacro(), and recInstMacros().

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

Expr CompleteInstPreProcessor::simplifyEq

(

const Expr &

)

simplify a=a to True

Definition at line 1455 of file theory_quant.cpp.

References CVC3::Expr::arity(), d_theoryCore, DebugAssert, std::endl(), CVC3::EXISTS, CVC3::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 &

)

put all quants in postive form and then skolemize all exists

Definition at line 1701 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 CVC3::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:

• theory_quant.h
• theory_quant.cpp

---