theory_quant.cpp File Reference

Go to the source code of this file.

Functions

• bool canGetHead (const Expr &e)
• static void recursiveGetSubTerm (const Expr &e, std::vector< Expr > &res)
• std::vector< Expr > getSubTerms (const Expr &e)
• static void recursiveGetBoundVars (const Expr &e, std::set< Expr > &result)

  get the bound vars in term e,
  

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

  get bound vars in term e,
  

• bool isGoodTrigger (const Expr &e, const std::vector< Expr > &bVarsThm)
• bool inStrCache (std::set< std::string > cache, std::string str)
• void genInstSetThm (const std::vector< Expr > &bVarsThm, const std::vector< Expr > &bVarsTerm, const std::set< std::vector< Expr > > &termInst, std::set< std::vector< Expr > > &instSetThm)

---

Detailed Description

Author: Daniel Wichs

Created: Wednesday July 2, 2003

---

Copyright (C) 2003 by the Board of Trustees of Leland Stanford Junior University and by New York University.

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. In particular:

• The above copyright notice and this permission notice must appear in all copies of the software and related documentation.

• THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES, EXPRESSED OR IMPLIED. USE IT AT YOUR OWN RISK.

---

Definition in file theory_quant.cpp.

---

Function Documentation

bool canGetHead (  const Expr &  e  )

Definition at line 98 of file theory_quant.cpp. References CVCL::Expr::getKind(), and CVCL::UFUNC. Referenced by CVCL::TheoryQuant::goodSynMatch(), isGoodTrigger(), CVCL::TheoryQuant::recSynMatch(), and CVCL::TheoryQuant::semCheckSat().

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

Definition at line 128 of file theory_quant.cpp. References CVCL::Expr::begin(), CVCL::Expr::end(), CVCL::Expr::getBody(), CVCL::Expr::getFlag(), CVCL::Expr::getKind(), CVCL::Expr::isClosure(), CVCL::Expr::isTerm(), CVCL::Expr::isVar(), CVCL::RATIONAL_EXPR, and CVCL::Expr::setFlag(). Referenced by getSubTerms().

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

Definition at line 153 of file theory_quant.cpp. References CVCL::Expr::clearFlags(), recursiveGetSubTerm(), CVCL::Expr::toString(), and CVCL::TRACE. Referenced by CVCL::TheoryQuant::setupTriggers().

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

get the bound vars in term e, Definition at line 165 of file theory_quant.cpp. References CVCL::Expr::begin(), CVCL::BOUND_VAR, CVCL::Expr::end(), CVCL::Expr::getBody(), CVCL::Expr::getFlag(), CVCL::Expr::getKind(), CVCL::Expr::isClosure(), and CVCL::Expr::setFlag(). Referenced by getBoundVars().

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

get bound vars in term e, Definition at line 186 of file theory_quant.cpp. References CVCL::Expr::clearFlags(), and recursiveGetBoundVars(). Referenced by CVCL::TheoryQuant::hasGoodSemInst(), CVCL::TheoryQuant::hasGoodSynInst(), and isGoodTrigger().

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

Definition at line 195 of file theory_quant.cpp. References canGetHead(), and getBoundVars(). Referenced by CVCL::TheoryQuant::setupTriggers().

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

Definition at line 483 of file theory_quant.cpp. Referenced by CVCL::TheoryQuant::hasGoodSemInst().

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

Definition at line 513 of file theory_quant.cpp. Referenced by CVCL::TheoryQuant::semInst(), and CVCL::TheoryQuant::synInst().

---