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 dependency graph for theory_quant.cpp:

Go to the source code of this file.

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

bool isSysPred ( const Expr &  e  ) 

Definition at line 229 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::newTopMatch(), CVC3::TheoryQuant::recSynMatch(), recursiveGetSubTrig(), CVC3::TheoryQuant::setupTriggers(), trigInitScore(), and usefulInMatch().

bool canGetHead ( const Expr &  e  ) 

Definition at line 233 of file theory_quant.cpp.

References CVC3::APPLY, CVC3::Expr::getKind(), CVC3::READ, and CVC3::WRITE.

Referenced by CVC3::TheoryQuant::canMatch(), CVC3::TheoryQuant::checkSat(), isSimpleTrig(), CVC3::TheoryQuant::isTransLike(), CVC3::TheoryQuant::recSynMatch(), CVC3::TheoryQuant::setupTriggers(), and usefulInMatch().

bool isSimpleTrig ( const Expr &  t  ) 

Definition at line 237 of file theory_quant.cpp.

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

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

bool isSuperSimpleTrig ( const Expr &  t  ) 

Definition at line 250 of file theory_quant.cpp.

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

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

bool usefulInMatch ( const Expr &  e  ) 

Definition at line 262 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 CVC3::TheoryQuant::goodSynMatch(), isGoodFullTrigger(), isGoodMultiTrigger(), isGoodPartTrigger(), isGoodSysPredTrigger(), and CVC3::TheoryQuant::synCheckSat().

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

Definition at line 275 of file theory_quant.cpp.

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

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

Definition at line 284 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 307 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 317 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 538 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 554 of file theory_quant.cpp.

References recursiveExprScore().

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

Expr getHeadExpr ( const Expr &  e  ) 

Definition at line 558 of file theory_quant.cpp.

References CVC3::APPLY, CVC3::Op::getExpr(), CVC3::Expr::getKind(), CVC3::Expr::getOp(), null_expr, CVC3::READ, CVC3::UCONST, CVC3::UFUNC, and CVC3::WRITE.

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

Expr getHead ( const Expr &  e  ) 

Definition at line 579 of file theory_quant.cpp.

References getHeadExpr().

Referenced by CVC3::TheoryQuant::canMatch(), CVC3::TheoryQuant::checkSat(), CVC3::TheoryQuant::isTransLike(), CVC3::TheoryQuant::matchListNew(), CVC3::TheoryQuant::matchListOld(), CVC3::TheoryQuant::recSynMatch(), and CVC3::TheoryQuant::setupTriggers().

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

get the bound vars in term e,

Definition at line 584 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 617 of file theory_quant.cpp.

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

Referenced by CVC3::TheoryQuant::arrayIndexName(), CVC3::TheoryQuant::generalTrig(), goodMultiTriggers(), CVC3::TheoryQuant::hasGoodSynMultiInst(), hasMoreBVs(), isGoodFullTrigger(), isGoodMultiTrigger(), isGoodPartTrigger(), CVC3::TheoryQuant::isTransLike(), and CVC3::TheoryQuant::setupTriggers().

bool isGoodSysPredTrigger ( const Expr &  e  ) 

Definition at line 637 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 643 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 662 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 697 of file theory_quant.cpp.

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

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

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

Definition at line 735 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 780 of file theory_quant.cpp.

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

int trigInitScore ( const Expr &  e  ) 

Definition at line 788 of file theory_quant.cpp.

References isGoodSysPredTrigger(), and isSysPred().

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

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

Definition at line 797 of file theory_quant.cpp.

References CVC3::ExprMap< Data >::count(), DebugAssert, CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Neg, CVC3::Pos, CVC3::PosNeg, and CVC3::Ukn.

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

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

Definition at line 1102 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 1127 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 1611 of file theory_quant.cpp.

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

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

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

Definition at line 1755 of file theory_quant.cpp.

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

Referenced by CVC3::ArithTheoremProducerOld::darkGrayShadow2ab(), CVC3::ArithTheoremProducer::darkGrayShadow2ab(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ba(), CVC3::ArithTheoremProducer::darkGrayShadow2ba(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), getLeft(), getRight(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::TheoryQuant::newTopMatch(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryArithOld::processSimpleIntEq(), and CVC3::TheoryArithNew::processSimpleIntEq().

Expr getLeft ( const Expr &  e  ) 

Definition at line 1761 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::newTopMatch().

Expr getRight ( const Expr &  e  ) 

Definition at line 1794 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::newTopMatch().

bool inStrCache ( std::set< std::string >  cache,
std::string  str 
)

Definition at line 3410 of file theory_quant.cpp.

void genPartInstSetThm ( const std::vector< Expr > &  bVarsThm,
std::vector< Expr > &  bVarsTerm,
const std::vector< std::vector< Expr > > &  termInst,
std::vector< std::vector< Expr > > &  instSetThm 
)

Definition at line 3422 of file theory_quant.cpp.

References CVC3::ExprMap< Data >::count(), and DebugAssert.

void genInstSetThm ( const std::vector< Expr > &  bVarsThm,
const std::vector< Expr > &  bVarsTerm,
const std::vector< std::vector< Expr > > &  termInst,
std::vector< std::vector< Expr > > &  instSetThm 
)

Definition at line 3461 of file theory_quant.cpp.

References DebugAssert.

Variable Documentation

const Expr null_expr [static]

Definition at line 40 of file theory_quant.cpp.

Referenced by CVC3::TheoryQuant::enqueueInst(), getHeadExpr(), getLeft(), getRight(), CVC3::TheoryQuant::matchListNew(), CVC3::TheoryQuant::matchListOld(), CVC3::TheoryQuant::newTopMatch(), CVC3::TheoryQuant::recGeneralTrig(), CVC3::TheoryQuant::recInstantiate(), CVC3::TheoryQuant::recSearchCover(), CVC3::TheoryQuant::registerTrig(), CVC3::TheoryQuant::searchCover(), CVC3::TheoryQuant::synNewInst(), and CVC3::Trigger::Trigger().

const int FOUND_FALSE = 1

Definition at line 41 of file theory_quant.cpp.

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

Generated on Tue Jul 3 14:35:12 2007 for CVC3 by  doxygen 1.5.1