CVC3  2.4.1
Public Member Functions | Private Member Functions | Private Attributes
CVC3::CompleteInstPreProcessor Class Reference

#include <theory_quant.h>

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

TheoryCored_theoryCore
QuantProofRulesd_quant_rules
std::set< Exprd_allIndex
ExprMap< Polarityd_expr_pol
ExprMap< Exprd_quant_equiv_map
std::vector< Exprd_gnd_cache
ExprMap< bool > d_is_macro_def
ExprMap< Exprd_macro_quant
ExprMap< Exprd_macro_def
ExprMap< Exprd_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
void CompleteInstPreProcessor::addIndex ( const Expr e)
private
void CompleteInstPreProcessor::collect_shield_index ( const Expr e)
private
void CompleteInstPreProcessor::collect_forall_index ( const Expr forall_quant)
private
bool CompleteInstPreProcessor::isGoodQuant ( const Expr e)
private
Expr CompleteInstPreProcessor::plusOne ( const Expr e)
private
Expr CompleteInstPreProcessor::minusOne ( const Expr e)
private
void CompleteInstPreProcessor::collectHeads ( const Expr assert,
std::set< Expr > &  heads 
)
private
bool CompleteInstPreProcessor::isMacro ( const Expr assert)
private
Expr CompleteInstPreProcessor::recInstMacros ( const Expr assert)
private
Expr CompleteInstPreProcessor::substMacro ( const Expr old)
private
Expr CompleteInstPreProcessor::recRewriteNot ( const Expr e,
ExprMap< Polarity > &  pol_map 
)
private
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
bool CompleteInstPreProcessor::isGood ( const Expr e)
void CompleteInstPreProcessor::collectIndex ( const Expr e)
Expr CompleteInstPreProcessor::inst ( const Expr e)
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)
Expr CompleteInstPreProcessor::simplifyQuant ( const Expr e)

Member Data Documentation

TheoryCore* CVC3::CompleteInstPreProcessor::d_theoryCore
private
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: