CVC3
Classes | Functions | Variables

theory_quant.cpp File Reference

#include "theory_quant.h"
#include "theory_arith.h"
#include "theory_array.h"
#include "typecheck_exception.h"
#include "parser_exception.h"
#include "smtlib_exception.h"
#include "quant_proof_rules.h"
#include "theory_core.h"
#include "command_line_flags.h"
#include "vcl.h"
#include <string>
#include <string.h>
#include <algorithm>
#include "assumptions.h"

Go to the source code of this file.

Classes

Functions

Variables

Function Documentation

std::string vectorExpr2string ( const std::vector< Expr > &  vec)

Definition at line 244 of file theory_quant.cpp.

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

bool isSysPred ( const Expr &  e)

Definition at line 278 of file theory_quant.cpp.

References CVC3::Expr::isEq(), CVC3::isGE(), CVC3::isGT(), CVC3::isLE(), and CVC3::isLT().

Referenced by isGoodMultiTrigger(), isGoodPartTrigger(), isGoodSysPredTrigger(), CVC3::TheoryQuant::newTopMatchNoSig(), CVC3::TheoryQuant::newTopMatchSig(), CVC3::TheoryQuant::recMultMatch(), CVC3::TheoryQuant::recMultMatchDebug(), CVC3::TheoryQuant::recMultMatchOldWay(), recursiveGetSubTrig(), CVC3::TheoryQuant::setupTriggers(), trigInitScore(), and usefulInMatch().

bool canGetHead ( const Expr &  e)

Definition at line 282 of file theory_quant.cpp.

References APPLY, CVC3::Expr::getKind(), CVC3::isDivide(), CVC3::isMinus(), CVC3::isMult(), CVC3::isPlus(), CVC3::isPow(), CVC3::READ, and CVC3::WRITE.

Referenced by CVC3::TheoryQuant::canMatch(), CVC3::TheoryQuant::checkSat(), isSimpleTrig(), CVC3::TheoryQuant::isTransLike(), CVC3::TheoryQuant::matchListOld(), CVC3::TheoryQuant::recMultMatch(), CVC3::TheoryQuant::recMultMatchDebug(), CVC3::TheoryQuant::recMultMatchOldWay(), CVC3::TheoryQuant::setupTriggers(), and usefulInMatch().

bool isSimpleTrig ( const Expr &  t)

Definition at line 295 of file theory_quant.cpp.

References CVC3::Expr::arity(), BOUND_VAR, canGetHead(), and CVC3::Expr::containsBoundVar().

Referenced by isSuperSimpleTrig(), and CVC3::TheoryQuant::setupTriggers().

bool isSuperSimpleTrig ( const Expr &  t)

Definition at line 308 of file theory_quant.cpp.

References CVC3::Expr::arity(), BOUND_VAR, CVC3::Expr::getKind(), isSimpleTrig(), CVC3::READ, and CVC3::WRITE.

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

bool usefulInMatch ( const Expr &  e)

Definition at line 323 of file theory_quant.cpp.

References CVC3::Expr::arity(), canGetHead(), CVC3::Expr::isEq(), CVC3::Expr::isRational(), isSysPred(), CVC3::Expr::toString(), and TRACE.

Referenced by isGoodFullTrigger(), isGoodMultiTrigger(), isGoodPartTrigger(), isGoodSysPredTrigger(), and CVC3::TheoryQuant::synCheckSat().

static void recursiveGetSubTrig ( const Expr &  e,
std::vector< Expr > &  res 
) [static]

Definition at line 563 of file theory_quant.cpp.

References CVC3::Expr::begin(), CVC3::Expr::end(), CVC3::Expr::getBody(), CVC3::Expr::getFlag(), CVC3::Expr::getKind(), CVC3::Expr::isApply(), CVC3::Expr::isClosure(), isSysPred(), CVC3::Expr::isTerm(), CVC3::Expr::isVar(), RATIONAL_EXPR, and CVC3::Expr::setFlag().

Referenced by getSubTrig().

std::vector<Expr> getSubTrig ( const Expr &  e)

Definition at line 586 of file theory_quant.cpp.

References CVC3::Expr::clearFlags(), recursiveGetSubTrig(), CVC3::Expr::toString(), and TRACE.

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

static void recGetSubTerms ( const Expr &  e,
std::vector< Expr > &  res 
) [static]

Definition at line 596 of file theory_quant.cpp.

References CVC3::Expr::begin(), CVC3::Expr::end(), CVC3::Expr::getBody(), CVC3::Expr::getFlag(), CVC3::Expr::isClosure(), and CVC3::Expr::setFlag().

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

int recursiveExprScore ( const Expr &  e)

Definition at line 1042 of file theory_quant.cpp.

References CVC3::Expr::arity(), CVC3::Expr::begin(), DebugAssert, CVC3::Expr::end(), and CVC3::Expr::isClosure().

Referenced by exprScore().

int exprScore ( const Expr &  e)

Definition at line 1059 of file theory_quant.cpp.

References recursiveExprScore().

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

static bool recursiveGetBoundVars ( const Expr &  e,
std::set< Expr > &  result 
) [static]

get the bound vars in term e,

Definition at line 1111 of file theory_quant.cpp.

References CVC3::Expr::begin(), BOUND_VAR, CVC3::Expr::containsBoundVar(), CVC3::Expr::end(), CVC3::Expr::getBody(), CVC3::Expr::getFlag(), CVC3::Expr::getKind(), CVC3::Expr::isClosure(), CVC3::Expr::setContainsBoundVar(), and CVC3::Expr::setFlag().

Referenced by getBoundVars().

std::set<Expr> getBoundVars ( const Expr &  e)

get bound vars in term e,

Definition at line 1144 of file theory_quant.cpp.

References CVC3::Expr::clearFlags(), and recursiveGetBoundVars().

Referenced by CVC3::TheoryQuant::arrayIndexName(), goodMultiTriggers(), hasMoreBVs(), CVC3::CompleteInstPreProcessor::isGood(), isGoodFullTrigger(), isGoodMultiTrigger(), isGoodPartTrigger(), CVC3::TheoryQuant::isTransLike(), CVC3::CompleteInstPreProcessor::rewriteNot(), CVC3::TheoryQuant::setupTriggers(), and CVC3::TheoryQuant::theoryPreprocess().

void findPolarity ( const Expr &  e,
ExprMap< Polarity > &  res,
Polarity  pol 
)

Definition at line 1166 of file theory_quant.cpp.

References CVC3::Expr::arity(), CVC3::ExprMap< Data >::count(), CVC3::Expr::getBody(), CVC3::Expr::getType(), CVC3::Expr::isAnd(), CVC3::Expr::isAtomicFormula(), CVC3::Type::isBool(), CVC3::Expr::isClosure(), CVC3::Expr::isIff(), CVC3::Expr::isImpl(), CVC3::Expr::isITE(), CVC3::Expr::isNot(), CVC3::Expr::isOr(), CVC3::Expr::isXor(), CVC3::Neg, CVC3::Pos, CVC3::PosNeg, TRACE, and CVC3::Ukn.

Referenced by CVC3::CompleteInstPreProcessor::collect_forall_index(), CVC3::CompleteInstPreProcessor::isGoodQuant(), CVC3::CompleteInstPreProcessor::rewriteNot(), CVC3::TheoryQuant::setupTriggers(), and CVC3::CompleteInstPreProcessor::simplifyQuant().

bool isUniterpFunc ( const Expr &  e)

Definition at line 1231 of file theory_quant.cpp.

References CVC3::Expr::getOpKind(), CVC3::Expr::isApply(), and UFUNC.

Referenced by CVC3::CompleteInstPreProcessor::collect_shield_index(), CVC3::CompleteInstPreProcessor::collectHeads(), CVC3::CompleteInstPreProcessor::hasShieldVar(), CVC3::CompleteInstPreProcessor::isMacro(), CVC3::CompleteInstPreProcessor::isShield(), and CVC3::CompleteInstPreProcessor::recInstMacros().

bool isGround ( const Expr &  e)

Definition at line 1243 of file theory_quant.cpp.

References CVC3::Expr::containsBoundVar().

Referenced by CVC3::CompleteInstPreProcessor::collect_forall_index(), CVC3::CompleteInstPreProcessor::collect_shield_index(), CVC3::CompleteInstPreProcessor::collectIndex(), CVC3::CompleteInstPreProcessor::inst(), CVC3::CompleteInstPreProcessor::isShield(), and CVC3::CompleteInstPreProcessor::recRewriteNot().

void findPolarityAtomic ( const Expr &  e,
ExprMap< Polarity > &  res,
Polarity  pol 
)

Definition at line 1626 of file theory_quant.cpp.

References CVC3::Expr::arity(), CVC3::ExprMap< Data >::count(), DebugAssert, CVC3::Expr::getType(), CVC3::Expr::isAnd(), CVC3::Expr::isAtomicFormula(), CVC3::Type::isBool(), CVC3::Expr::isClosure(), CVC3::Expr::isIff(), CVC3::Expr::isImpl(), CVC3::Expr::isITE(), CVC3::Expr::isNot(), CVC3::Expr::isOr(), CVC3::Expr::isXor(), CVC3::Neg, CVC3::Pos, CVC3::PosNeg, CVC3::Expr::toString(), and CVC3::Ukn.

Referenced by CVC3::CompleteInstPreProcessor::collectIndex(), and CVC3::CompleteInstPreProcessor::isGood().

void flatAnds ( const Expr &  ands,
vector< Expr > &  results 
)

Definition at line 2322 of file theory_quant.cpp.

References CVC3::Expr::begin(), CVC3::Expr::end(), CVC3::Expr::isAnd(), CVC3::Expr::isNot(), and CVC3::Expr::isOr().

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

bool isGoodSysPredTrigger ( const Expr &  e)

Definition at line 2456 of file theory_quant.cpp.

References isSysPred(), and usefulInMatch().

Referenced by isGoodMultiTrigger(), isGoodPartTrigger(), and trigInitScore().

bool isGoodFullTrigger ( const Expr &  e,
const std::vector< Expr > &  bVarsThm 
)

Definition at line 2462 of file theory_quant.cpp.

References getBoundVars(), and usefulInMatch().

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

bool isGoodMultiTrigger ( const Expr &  e,
const std::vector< Expr > &  bVarsThm,
int  offset 
)

Definition at line 2481 of file theory_quant.cpp.

References getBoundVars(), isGoodSysPredTrigger(), isSysPred(), and usefulInMatch().

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

bool isGoodPartTrigger ( const Expr &  e,
const std::vector< Expr > &  bVarsThm 
)

Definition at line 2516 of file theory_quant.cpp.

References getBoundVars(), isGoodSysPredTrigger(), isSysPred(), and usefulInMatch().

static bool recursiveGetPartTriggers ( const Expr &  e,
std::vector< Expr > &  res 
) [static]

Definition at line 2554 of file theory_quant.cpp.

References CVC3::Expr::arity(), CVC3::Expr::begin(), BOUND_VAR, CVC3::Expr::end(), CVC3::Expr::getBody(), CVC3::Expr::getFlag(), CVC3::Expr::getKind(), CVC3::Expr::isClosure(), and CVC3::Expr::setFlag().

Referenced by getPartTriggers().

std::vector<Expr> getPartTriggers ( const Expr &  e)

Definition at line 2599 of file theory_quant.cpp.

References CVC3::Expr::clearFlags(), and recursiveGetPartTriggers().

int trigInitScore ( const Expr &  e)

Definition at line 2607 of file theory_quant.cpp.

References isGoodSysPredTrigger(), and isSysPred().

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

bool goodMultiTriggers ( const std::vector< Expr > &  exprs,
const std::vector< Expr >  bVars 
)

Definition at line 2882 of file theory_quant.cpp.

References CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), and getBoundVars().

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

size_t locVar ( const vector< Expr > &  bvsThm,
const Expr &  bv 
) [inline]

Definition at line 2907 of file theory_quant.cpp.

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

int hasMoreBVs ( const Expr &  thm)

test if a sub-term contains more bounded vars than quantified by out-most quantifier.

Definition at line 3483 of file theory_quant.cpp.

References DebugAssert, getBoundVars(), CVC3::Expr::getVars(), and CVC3::Expr::isForall().

bool isIntx ( const Expr &  e,
const Rational &  x 
)

Definition at line 3731 of file theory_quant.cpp.

References CVC3::Expr::getRational(), and CVC3::Expr::isRational().

Referenced by CVC3::TheoryArith3::doSolve(), getLeft(), getRight(), CVC3::TheoryQuant::newTopMatchNoSig(), CVC3::TheoryQuant::newTopMatchSig(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryArith3::normalizeProjectIneqs(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithNew::processSimpleIntEq(), and CVC3::TheoryArith3::processSimpleIntEq().

Expr getLeft ( const Expr &  e)

Definition at line 3738 of file theory_quant.cpp.

References CVC3::Expr::arity(), CVC3::Expr::getKind(), isIntx(), CVC3::isRational(), CVC3::MULT, null_expr, and CVC3::PLUS.

Referenced by CVC3::TheoryQuant::newTopMatchNoSig(), and CVC3::TheoryQuant::newTopMatchSig().

Expr getRight ( const Expr &  e)

Definition at line 3771 of file theory_quant.cpp.

References CVC3::Expr::arity(), CVC3::Expr::getKind(), isIntx(), CVC3::isRational(), CVC3::MULT, null_expr, and CVC3::PLUS.

Referenced by CVC3::TheoryQuant::newTopMatchNoSig(), and CVC3::TheoryQuant::newTopMatchSig().

bool cmpExpr ( Expr  e1,
Expr  e2 
)

Definition at line 5293 of file theory_quant.cpp.

References CVC3::Expr::getIndex(), and CVC3::Expr::isNull().

Variable Documentation

const Expr null_expr [static]

Definition at line 42 of file theory_quant.cpp.

Referenced by CVC3::TheoryQuant::enqueueInst(), CVC3::TheoryQuant::getHeadExpr(), getLeft(), getRight(), CVC3::TheoryQuant::matchListNew(), CVC3::TheoryQuant::matchListOld(), CVC3::TheoryQuant::newTopMatchNoSig(), CVC3::TheoryQuant::newTopMatchSig(), CVC3::TheoryQuant::recInstantiate(), CVC3::TheoryQuant::simpRAWList(), CVC3::TheoryQuant::synNewInst(), CVC3::TheoryQuant::TheoryQuant(), and CVC3::Trigger::Trigger().

const int FOUND_FALSE = 1

Definition at line 43 of file theory_quant.cpp.

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

Generated on Thu Sep 1 2011 19:35:07 for CVC3 by  doxygen 1.7.3