CVC3  2.4.1
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

class  recCompleteInster
 

Functions

std::string vectorExpr2string (const std::vector< Expr > &vec)
 
bool isSysPred (const Expr &e)
 
bool canGetHead (const Expr &e)
 
bool isSimpleTrig (const Expr &t)
 
bool isSuperSimpleTrig (const Expr &t)
 
bool usefulInMatch (const Expr &e)
 
static void recursiveGetSubTrig (const Expr &e, std::vector< Expr > &res)
 
std::vector< ExprgetSubTrig (const Expr &e)
 
static void recGetSubTerms (const Expr &e, std::vector< Expr > &res)
 
int recursiveExprScore (const Expr &e)
 
int exprScore (const Expr &e)
 
static bool recursiveGetBoundVars (const Expr &e, std::set< Expr > &result)
 get the bound vars in term e, More...
 
std::set< ExprgetBoundVars (const Expr &e)
 get bound vars in term e, More...
 
void findPolarity (const Expr &e, ExprMap< Polarity > &res, Polarity pol)
 
bool isUniterpFunc (const Expr &e)
 
bool isGround (const Expr &e)
 
void findPolarityAtomic (const Expr &e, ExprMap< Polarity > &res, Polarity pol)
 
void flatAnds (const Expr &ands, vector< Expr > &results)
 
bool isGoodSysPredTrigger (const Expr &e)
 
bool isGoodFullTrigger (const Expr &e, const std::vector< Expr > &bVarsThm)
 
bool isGoodMultiTrigger (const Expr &e, const std::vector< Expr > &bVarsThm, int offset)
 
bool isGoodPartTrigger (const Expr &e, const std::vector< Expr > &bVarsThm)
 
static bool recursiveGetPartTriggers (const Expr &e, std::vector< Expr > &res)
 
std::vector< ExprgetPartTriggers (const Expr &e)
 
int trigInitScore (const Expr &e)
 
bool goodMultiTriggers (const std::vector< Expr > &exprs, const std::vector< Expr > bVars)
 
size_t locVar (const vector< Expr > &bvsThm, const Expr &bv)
 
int hasMoreBVs (const Expr &thm)
 test if a sub-term contains more bounded vars than quantified by out-most quantifier. More...
 
bool isIntx (const Expr &e, const Rational &x)
 
Expr getLeft (const Expr &e)
 
Expr getRight (const Expr &e)
 
bool cmpExpr (Expr e1, Expr e2)
 

Variables

static const Expr null_expr
 
const int FOUND_FALSE = 1
 

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)
bool canGetHead ( const Expr e)
bool isSimpleTrig ( const Expr t)
bool isSuperSimpleTrig ( const Expr t)
bool usefulInMatch ( const Expr e)
static void recursiveGetSubTrig ( const Expr e,
std::vector< Expr > &  res 
)
static
std::vector<Expr> getSubTrig ( const Expr e)
static void recGetSubTerms ( const Expr e,
std::vector< Expr > &  res 
)
static
int recursiveExprScore ( const Expr e)
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
std::set<Expr> getBoundVars ( const Expr e)
void findPolarity ( const Expr e,
ExprMap< Polarity > &  res,
Polarity  pol 
)
bool isUniterpFunc ( const Expr e)
bool isGround ( const Expr e)
void findPolarityAtomic ( const Expr e,
ExprMap< Polarity > &  res,
Polarity  pol 
)
void flatAnds ( const Expr ands,
vector< Expr > &  results 
)
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 
)
bool isGoodPartTrigger ( const Expr e,
const std::vector< Expr > &  bVarsThm 
)
static bool recursiveGetPartTriggers ( const Expr e,
std::vector< Expr > &  res 
)
static
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 
)
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 
)
Expr getLeft ( const Expr e)
Expr getRight ( const Expr e)
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
const int FOUND_FALSE = 1

Definition at line 43 of file theory_quant.cpp.

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