CVC3::CompleteInstPreProcessor Class Reference

#include <theory_quant.h>

Collaboration diagram for CVC3::CompleteInstPreProcessor:

Collaboration graph
[legend]

List of all members.

Public Member Functions

Private Member Functions

Private Attributes


Detailed Description

Definition at line 97 of file theory_quant.h.


Constructor & Destructor Documentation

CompleteInstPreProcessor::CompleteInstPreProcessor ( TheoryCore core,
QuantProofRules quant_rule 
)

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

Referenced by collect_forall_index(), and isGoodQuant().

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 1726 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 1414 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 1537 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

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.

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(), recInstMacros(), and substMacro().

Definition at line 116 of file theory_quant.h.

Referenced by isMacro(), and substMacro().

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:

Generated on Thu Oct 15 22:22:53 2009 for CVC3 by  doxygen 1.5.8