CVC3
2.4.1
|
#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.
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::isLE(), CVC3::isLT(), CVC3::isGE(), CVC3::isGT(), and CVC3::Expr::isEq().
Referenced by usefulInMatch(), recursiveGetSubTrig(), isGoodSysPredTrigger(), isGoodMultiTrigger(), isGoodPartTrigger(), trigInitScore(), CVC3::TheoryQuant::setupTriggers(), CVC3::TheoryQuant::newTopMatchNoSig(), CVC3::TheoryQuant::newTopMatchSig(), CVC3::TheoryQuant::recMultMatchDebug(), CVC3::TheoryQuant::recMultMatchOldWay(), and CVC3::TheoryQuant::recMultMatch().
bool canGetHead | ( | const Expr & | e | ) |
Definition at line 282 of file theory_quant.cpp.
References CVC3::Expr::getKind(), APPLY, CVC3::READ, CVC3::WRITE, CVC3::isPlus(), CVC3::isMinus(), CVC3::isMult(), CVC3::isDivide(), and CVC3::isPow().
Referenced by isSimpleTrig(), usefulInMatch(), CVC3::TheoryQuant::canMatch(), CVC3::TheoryQuant::isTransLike(), CVC3::TheoryQuant::setupTriggers(), CVC3::TheoryQuant::matchListOld(), CVC3::TheoryQuant::recMultMatchDebug(), CVC3::TheoryQuant::recMultMatchOldWay(), CVC3::TheoryQuant::recMultMatch(), and CVC3::TheoryQuant::checkSat().
bool isSimpleTrig | ( | const Expr & | t | ) |
Definition at line 295 of file theory_quant.cpp.
References canGetHead(), CVC3::Expr::arity(), CVC3::Expr::containsBoundVar(), and BOUND_VAR.
Referenced by isSuperSimpleTrig(), and CVC3::TheoryQuant::setupTriggers().
bool isSuperSimpleTrig | ( | const Expr & | t | ) |
Definition at line 308 of file theory_quant.cpp.
References isSimpleTrig(), CVC3::Expr::getKind(), CVC3::READ, CVC3::WRITE, CVC3::Expr::arity(), and BOUND_VAR.
Referenced by CVC3::TheoryQuant::setupTriggers().
bool usefulInMatch | ( | const Expr & | e | ) |
Definition at line 323 of file theory_quant.cpp.
References CVC3::Expr::arity(), TRACE, CVC3::Expr::toString(), CVC3::Expr::isRational(), canGetHead(), isSysPred(), and CVC3::Expr::isEq().
Referenced by isGoodSysPredTrigger(), isGoodFullTrigger(), isGoodMultiTrigger(), isGoodPartTrigger(), 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::getFlag(), CVC3::Expr::isClosure(), CVC3::Expr::getBody(), CVC3::Expr::isApply(), isSysPred(), CVC3::Expr::isTerm(), CVC3::Expr::isVar(), CVC3::Expr::getKind(), RATIONAL_EXPR, CVC3::Expr::begin(), CVC3::Expr::end(), 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(), TRACE, and CVC3::Expr::toString().
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::getFlag(), CVC3::Expr::isClosure(), CVC3::Expr::getBody(), CVC3::Expr::begin(), CVC3::Expr::end(), and CVC3::Expr::setFlag().
Referenced by CVC3::TheoryQuant::getSubTerms().
int recursiveExprScore | ( | const Expr & | e | ) |
Definition at line 1042 of file theory_quant.cpp.
References DebugAssert, CVC3::Expr::isClosure(), CVC3::Expr::arity(), CVC3::Expr::begin(), and CVC3::Expr::end().
Referenced by exprScore().
int exprScore | ( | const Expr & | e | ) |
Definition at line 1059 of file theory_quant.cpp.
References recursiveExprScore().
Referenced by CVC3::TheoryQuant::setupTriggers().
get the bound vars in term e,
Definition at line 1111 of file theory_quant.cpp.
References CVC3::Expr::getFlag(), CVC3::Expr::containsBoundVar(), CVC3::Expr::isClosure(), CVC3::Expr::getBody(), BOUND_VAR, CVC3::Expr::getKind(), CVC3::Expr::setContainsBoundVar(), CVC3::Expr::begin(), CVC3::Expr::end(), and CVC3::Expr::setFlag().
Referenced by getBoundVars().
get bound vars in term e,
Definition at line 1144 of file theory_quant.cpp.
References CVC3::Expr::clearFlags(), and recursiveGetBoundVars().
Referenced by CVC3::CompleteInstPreProcessor::rewriteNot(), CVC3::CompleteInstPreProcessor::isGood(), CVC3::TheoryQuant::theoryPreprocess(), isGoodFullTrigger(), isGoodMultiTrigger(), isGoodPartTrigger(), CVC3::TheoryQuant::arrayIndexName(), CVC3::TheoryQuant::isTransLike(), goodMultiTriggers(), CVC3::TheoryQuant::setupTriggers(), and hasMoreBVs().
Definition at line 1166 of file theory_quant.cpp.
References CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::ExprMap::count(), CVC3::Neg, CVC3::Pos, CVC3::PosNeg, TRACE, CVC3::Expr::arity(), CVC3::Ukn, CVC3::Expr::isImpl(), CVC3::Expr::isAnd(), CVC3::Expr::isOr(), CVC3::Expr::isNot(), CVC3::Expr::isITE(), CVC3::Expr::isClosure(), CVC3::Expr::getBody(), CVC3::Expr::isIff(), CVC3::Expr::isXor(), and CVC3::Expr::isAtomicFormula().
Referenced by CVC3::CompleteInstPreProcessor::simplifyQuant(), CVC3::CompleteInstPreProcessor::rewriteNot(), CVC3::CompleteInstPreProcessor::collect_forall_index(), CVC3::CompleteInstPreProcessor::isGoodQuant(), and CVC3::TheoryQuant::setupTriggers().
bool isUniterpFunc | ( | const Expr & | e | ) |
Definition at line 1231 of file theory_quant.cpp.
References CVC3::Expr::isApply(), CVC3::Expr::getOpKind(), and UFUNC.
Referenced by CVC3::CompleteInstPreProcessor::collectHeads(), CVC3::CompleteInstPreProcessor::isMacro(), CVC3::CompleteInstPreProcessor::recInstMacros(), CVC3::CompleteInstPreProcessor::hasShieldVar(), CVC3::CompleteInstPreProcessor::isShield(), and CVC3::CompleteInstPreProcessor::collect_shield_index().
bool isGround | ( | const Expr & | e | ) |
Definition at line 1243 of file theory_quant.cpp.
References CVC3::Expr::containsBoundVar().
Referenced by CVC3::CompleteInstPreProcessor::isShield(), CVC3::CompleteInstPreProcessor::recRewriteNot(), CVC3::CompleteInstPreProcessor::collect_shield_index(), CVC3::CompleteInstPreProcessor::collect_forall_index(), CVC3::CompleteInstPreProcessor::collectIndex(), and CVC3::CompleteInstPreProcessor::inst().
Definition at line 1626 of file theory_quant.cpp.
References CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::ExprMap::count(), CVC3::Neg, CVC3::Pos, CVC3::PosNeg, CVC3::Expr::arity(), CVC3::Ukn, CVC3::Expr::isImpl(), CVC3::Expr::isAnd(), CVC3::Expr::isOr(), CVC3::Expr::isNot(), CVC3::Expr::isITE(), CVC3::Expr::isClosure(), CVC3::Expr::isIff(), CVC3::Expr::isXor(), CVC3::Expr::isAtomicFormula(), DebugAssert, and CVC3::Expr::toString().
Referenced by CVC3::CompleteInstPreProcessor::collectIndex(), and CVC3::CompleteInstPreProcessor::isGood().
Definition at line 2322 of file theory_quant.cpp.
References CVC3::Expr::isAnd(), CVC3::Expr::begin(), CVC3::Expr::end(), 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 usefulInMatch(), and getBoundVars().
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 usefulInMatch(), getBoundVars(), isSysPred(), and isGoodSysPredTrigger().
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 usefulInMatch(), getBoundVars(), isSysPred(), and isGoodSysPredTrigger().
static bool recursiveGetPartTriggers | ( | const Expr & | e, |
std::vector< Expr > & | res | ||
) | [static] |
Definition at line 2554 of file theory_quant.cpp.
References CVC3::Expr::getFlag(), CVC3::Expr::isClosure(), CVC3::Expr::getBody(), CVC3::Expr::arity(), BOUND_VAR, CVC3::Expr::getKind(), CVC3::Expr::begin(), CVC3::Expr::end(), 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 isSysPred(), and isGoodSysPredTrigger().
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 getBoundVars(), CVC3::ExprMap::find(), and CVC3::ExprMap::end().
Referenced by CVC3::TheoryQuant::setupTriggers().
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, CVC3::Expr::isForall(), CVC3::Expr::getVars(), and getBoundVars().
Definition at line 3731 of file theory_quant.cpp.
References CVC3::Expr::isRational(), and CVC3::Expr::getRational().
Referenced by CVC3::TheoryArith3::doSolve(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryArith3::normalizeProjectIneqs(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithOld::normalizeProjectIneqs(), getLeft(), getRight(), CVC3::TheoryQuant::newTopMatchNoSig(), and CVC3::TheoryQuant::newTopMatchSig().
Definition at line 3738 of file theory_quant.cpp.
References CVC3::Expr::getKind(), CVC3::PLUS, null_expr, CVC3::Expr::arity(), CVC3::MULT, isIntx(), and CVC3::isRational().
Referenced by CVC3::TheoryQuant::newTopMatchNoSig(), and CVC3::TheoryQuant::newTopMatchSig().
Definition at line 3771 of file theory_quant.cpp.
References CVC3::Expr::getKind(), CVC3::PLUS, null_expr, CVC3::Expr::arity(), CVC3::MULT, isIntx(), and CVC3::isRational().
Referenced by CVC3::TheoryQuant::newTopMatchNoSig(), and CVC3::TheoryQuant::newTopMatchSig().
Definition at line 5293 of file theory_quant.cpp.
References CVC3::Expr::isNull(), and CVC3::Expr::getIndex().
Definition at line 42 of file theory_quant.cpp.
Referenced by CVC3::Trigger::Trigger(), CVC3::TheoryQuant::TheoryQuant(), CVC3::TheoryQuant::enqueueInst(), CVC3::TheoryQuant::getHeadExpr(), getLeft(), getRight(), CVC3::TheoryQuant::matchListOld(), CVC3::TheoryQuant::matchListNew(), CVC3::TheoryQuant::newTopMatchNoSig(), CVC3::TheoryQuant::newTopMatchSig(), CVC3::TheoryQuant::simpRAWList(), CVC3::TheoryQuant::synNewInst(), and CVC3::TheoryQuant::recInstantiate().
const int FOUND_FALSE = 1 |
Definition at line 43 of file theory_quant.cpp.
Referenced by CVC3::TheoryQuant::enqueueInst().