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"

Include dependency graph for theory_quant.cpp:

Go to the source code of this file.

Classes

Functions

Variables

Detailed Description

Author: Daniel Wichs, Yeting Ge

Created: Wednesday July 2, 2003

License to use, copy, modify, sell and/or distribute this software and its documentation for any purpose is hereby granted without royalty, subject to the terms and conditions defined in the LICENSE file provided with this distribution.

Definition in file theory_quant.cpp.

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 CVC3::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(), CVC3::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(), CVC3::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 CVC3::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 556 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(), CVC3::RATIONAL_EXPR, and CVC3::Expr::setFlag().

Referenced by getSubTrig().

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

Definition at line 579 of file theory_quant.cpp.

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

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

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

Definition at line 589 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 1035 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 1052 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 1104 of file theory_quant.cpp.

References CVC3::Expr::begin(), CVC3::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 1137 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 1159 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, CVC3::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 1224 of file theory_quant.cpp.

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

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

bool isGround ( const Expr &  e  ) 

Definition at line 1236 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 1596 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 2269 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 2402 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 2408 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 2427 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 2462 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 2500 of file theory_quant.cpp.

References CVC3::Expr::arity(), CVC3::Expr::begin(), CVC3::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 2545 of file theory_quant.cpp.

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

int trigInitScore ( const Expr &  e  ) 

Definition at line 2553 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 2828 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 2853 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 3416 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 3600 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 3607 of file theory_quant.cpp.

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

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

Expr getRight ( const Expr &  e  ) 

Definition at line 3640 of file theory_quant.cpp.

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

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

bool cmpExpr ( Expr  e1,
Expr  e2 
)

Definition at line 5162 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.

const int FOUND_FALSE = 1

Definition at line 43 of file theory_quant.cpp.

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

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