This makes it so that TermUtil is now a collection of static methods. Further refactoring will make this a standalone file of utility methods.
This breaks all dependencies on the TermUtil object in QuantifiersEngine. It also starts breaking some of the depenendencies on quantifiers engine in sygus.
#include "theory/datatypes/sygus_simple_sym.h"
+#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
using namespace std;
namespace datatypes {
SygusSimpleSymBreak::SygusSimpleSymBreak(QuantifiersEngine* qe)
- : d_tds(qe->getTermDatabaseSygus()), d_tutil(qe->getTermUtil())
+ : d_tds(qe->getTermDatabaseSygus())
{
}
{
Kind ok;
int offset;
- if (d_tutil->hasOffsetArg(pk, arg, offset, ok))
+ if (quantifiers::TermUtil::hasOffsetArg(pk, arg, offset, ok))
{
Trace("sygus-sb-simple-debug")
<< pk << " has offset arg " << ok << " " << offset << std::endl;
if (d_tds->isTypeMatch(pdt[ok_arg], pdt[arg]))
{
int status;
- Node co = d_tutil->getTypeValueOffset(c.getType(), c, offset, status);
+ Node co = quantifiers::TermUtil::mkTypeValueOffset(
+ c.getType(), c, offset, status);
Trace("sygus-sb-simple-debug")
<< c << " with offset " << offset << " is " << co
<< ", status=" << status << std::endl;
bool ret = true;
Trace("sygus-sb-debug") << "Consider sygus const " << c << ", parent = " << pk
<< ", arg = " << arg << "?" << std::endl;
- if (d_tutil->isIdempotentArg(c, pk, arg))
+ if (quantifiers::TermUtil::isIdempotentArg(c, pk, arg))
{
if (pdt[pc].getNumArgs() == 2)
{
}
else
{
- Node sc = d_tutil->isSingularArg(c, pk, arg);
+ Node sc = quantifiers::TermUtil::isSingularArg(c, pk, arg);
if (!sc.isNull())
{
if (pti.hasConst(sc))
{
ReqTrie rt;
Assert(rt.empty());
- Node max_c = d_tutil->getTypeMaxValue(c.getType());
- Node zero_c = d_tutil->getTypeValue(c.getType(), 0);
- Node one_c = d_tutil->getTypeValue(c.getType(), 1);
+ Node max_c = quantifiers::TermUtil::mkTypeMaxValue(c.getType());
+ Node zero_c = quantifiers::TermUtil::mkTypeValue(c.getType(), 0);
+ Node one_c = quantifiers::TermUtil::mkTypeValue(c.getType(), 1);
if (pk == XOR || pk == BITVECTOR_XOR)
{
if (c == max_c)
#include <map>
#include "expr/dtype.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
-#include "theory/quantifiers/term_util.h"
namespace CVC4 {
namespace theory {
private:
/** Pointer to the sygus term database */
quantifiers::TermDbSygus* d_tds;
- /** Pointer to the quantifiers term utility */
- quantifiers::TermUtil* d_tutil;
/** return the index of the first argument position of c that has type tn */
int getFirstArgOccurrence(const DTypeConstructor& c, TypeNode tn);
/**
{
// redo, split integer/non-integer parts
bool useCoeff = false;
- Integer coeff = ci->getQuantifiersEngine()
- ->getTermUtil()
- ->d_one.getConst<Rational>()
- .getNumerator();
+ Integer coeff(1);
for (std::map<Node, Node>::iterator it = msum.begin(); it != msum.end();
++it)
{
bool pol = lit.getKind()!=NOT;
//arithmetic inequalities and disequalities
if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol && atom[0].getType().isReal() ) ){
+ NodeManager* nm = NodeManager::currentNM();
Assert(atom.getKind() != GEQ || atom[1].isConst());
Node atom_lhs;
Node atom_rhs;
atom_lhs = atom[0];
atom_rhs = atom[1];
}else{
- atom_lhs = NodeManager::currentNM()->mkNode( MINUS, atom[0], atom[1] );
+ atom_lhs = nm->mkNode(MINUS, atom[0], atom[1]);
atom_lhs = Rewriter::rewrite( atom_lhs );
- atom_rhs = getQuantifiersEngine()->getTermUtil()->d_zero;
+ atom_rhs = nm->mkConst(Rational(0));
}
//must be an eligible term
if( isEligible( atom_lhs ) ){
//apply substitution to LHS of atom
TermProperties atom_lhs_prop;
- atom_lhs = applySubstitution( NodeManager::currentNM()->realType(), atom_lhs, vars, subs, prop, non_basic, atom_lhs_prop );
+ atom_lhs = applySubstitution(nm->realType(),
+ atom_lhs,
+ vars,
+ subs,
+ prop,
+ non_basic,
+ atom_lhs_prop);
if( !atom_lhs.isNull() ){
if( !atom_lhs_prop.d_coeff.isNull() ){
- atom_rhs = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, atom_lhs_prop.d_coeff, atom_rhs ) );
+ atom_rhs = nm->mkNode(MULT, atom_lhs_prop.d_coeff, atom_rhs);
+ atom_rhs = Rewriter::rewrite(atom_rhs);
}
- lret = NodeManager::currentNM()->mkNode( atom.getKind(), atom_lhs, atom_rhs );
+ lret = nm->mkNode(atom.getKind(), atom_lhs, atom_rhs);
if( !pol ){
lret = lret.negate();
}
Node tu = u;
getBounds( q, v, rsi, tl, tu );
Assert(!tl.isNull() && !tu.isNull());
- if( ra==d_quantEngine->getTermUtil()->d_true ){
+ if (ra.isConst() && ra.getConst<bool>())
+ {
long rr = range.getConst<Rational>().getNumerator().getLong()+1;
Trace("bound-int-rsi") << "Actual bound range is " << rr << std::endl;
for( unsigned k=0; k<rr; k++ ){
return d_quantEngine->getTermDatabase();
}
-quantifiers::TermUtil* QuantifiersModule::getTermUtil() const
-{
- return d_quantEngine->getTermUtil();
-}
-
quantifiers::QuantifiersState& QuantifiersModule::getState()
{
return d_qstate;
namespace quantifiers {
class TermDb;
-class TermUtil;
} // namespace quantifiers
/** QuantifiersModule class
QuantifiersEngine* getQuantifiersEngine() const;
/** get currently used term database */
quantifiers::TermDb* getTermDatabase() const;
- /** get currently used term utility object */
- quantifiers::TermUtil* getTermUtil() const;
/** get the quantifiers state */
quantifiers::QuantifiersState& getState();
/** get the quantifiers inference manager */
}
if( !eq.isNull() ){
eq = Rewriter::rewrite( eq );
- if( eq!=d_qe->getTermUtil()->d_true ){
+ if (!eq.isConst() || !eq.getConst<bool>())
+ {
success = false;
break;
}
TypeNode btn = dt.getSygusType();
// for constant reconstruction
Kind ck = getComparisonKind(btn);
- Node z = d_qe->getTermUtil()->getTypeValue(btn, 0);
+ Node z = TermUtil::mkTypeValue(btn, 0);
// iterate over constructors
for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
#include "theory/quantifiers/sygus/synth_conjecture.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
#include "theory/strings/word.h"
using namespace CVC4::kind;
namespace theory {
namespace quantifiers {
-CegGrammarConstructor::CegGrammarConstructor(QuantifiersEngine* qe,
+CegGrammarConstructor::CegGrammarConstructor(TermDbSygus* tds,
SynthConjecture* p)
- : d_qe(qe), d_parent(p), d_is_syntax_restricted(false)
+ : d_tds(tds), d_parent(p), d_is_syntax_restricted(false)
{
}
sfvl = preGrammarType.getDType().getSygusVarList();
tn = preGrammarType;
// normalize type, if user-provided
- SygusGrammarNorm sygus_norm(d_qe);
+ SygusGrammarNorm sygus_norm(d_tds);
tn = sygus_norm.normalizeSygusType(tn, sfvl);
}else{
sfvl = SygusUtils::getSygusArgumentListForSynthFun(sf);
std::vector<Node> qchildren;
Node qbody_subs = q[1];
- TermDbSygus* tds = d_qe->getTermDatabaseSygus();
for (unsigned i = 0, size = q[0].getNumChildren(); i < size; i++)
{
Node sf = q[0][i];
Trace("cegqi-debug") << " body is now : " << qbody_subs << std::endl;
}
}
- tds->registerSygusType(tn);
+ d_tds->registerSygusType(tn);
Assert(tn.isDatatype());
const DType& dt = tn.getDType();
Assert(dt.isSygus());
std::stack<TNode> visit;
TNode cur;
visit.push(n);
- TermDbSygus* tds = d_qe->getTermDatabaseSygus();
do {
cur = visit.top();
visit.pop();
// lambda x1...xn. (DT_SYGUS_EVAL ef x1 ... xn)
// where ef is the first order variable for the
// function-to-synthesize.
- SygusTypeInfo& ti = tds->getTypeInfo(ef.getType());
+ SygusTypeInfo& ti = d_tds->getTypeInfo(ef.getType());
const std::vector<Node>& vars = ti.getVarList();
Assert(!vars.empty());
std::vector<Node> vs;
namespace CVC4 {
namespace theory {
-class QuantifiersEngine;
-
/**
* Attribute for associating a function-to-synthesize with a first order
* variable whose type is a sygus datatype type that encodes its grammar.
namespace quantifiers {
class SynthConjecture;
+class TermDbSygus;
/**
* Utility for constructing datatypes that correspond to syntactic restrictions,
class CegGrammarConstructor
{
public:
- CegGrammarConstructor(QuantifiersEngine* qe, SynthConjecture* p);
+ CegGrammarConstructor(TermDbSygus* tds, SynthConjecture* p);
~CegGrammarConstructor() {}
/** process
*
Node convertToEmbedding(Node n);
private:
- /** reference to quantifier engine */
- QuantifiersEngine * d_qe;
+ /** The sygus term database we are using */
+ TermDbSygus* d_tds;
/** parent conjecture
* This contains global information about the synthesis conjecture.
*/
#include "theory/quantifiers/sygus/sygus_grammar_red.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
#include <numeric> // for std::iota
return d_children[op_pos[ind]].getOrMakeType(tn, unres_tn, op_pos, ind + 1);
}
-SygusGrammarNorm::SygusGrammarNorm(QuantifiersEngine* qe)
- : d_qe(qe), d_tds(d_qe->getTermDatabaseSygus())
-{
-}
+SygusGrammarNorm::SygusGrammarNorm(TermDbSygus* tds) : d_tds(tds) {}
SygusGrammarNorm::TypeObject::TypeObject(TypeNode src_tn, TypeNode unres_tn)
: d_tn(src_tn),
if (options::sygusMinGrammar() && dt.getNumConstructors() == op_pos.size())
{
SygusRedundantCons src;
- src.initialize(d_qe, tn);
+ src.initialize(d_tds, tn);
std::vector<unsigned> rindices;
src.getRedundant(rindices);
if (!rindices.empty())
#include "expr/node.h"
#include "expr/sygus_datatype.h"
#include "expr/type_node.h"
-#include "theory/quantifiers/term_util.h"
namespace CVC4 {
namespace theory {
class SygusGrammarNorm
{
public:
- SygusGrammarNorm(QuantifiersEngine* qe);
+ SygusGrammarNorm(TermDbSygus* tds);
~SygusGrammarNorm() {}
/** creates a normalized typenode from a given one.
*
}; /* class TransfChain */
- /** reference to quantifier engine */
- QuantifiersEngine* d_qe;
/** sygus term database associated with this utility */
TermDbSygus* d_tds;
/** List of variable inputs of function-to-synthesize.
#include "options/quantifiers_options.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
using namespace std;
using namespace CVC4::kind;
namespace theory {
namespace quantifiers {
-void SygusRedundantCons::initialize(QuantifiersEngine* qe, TypeNode tn)
+void SygusRedundantCons::initialize(TermDbSygus* tds, TypeNode tn)
{
- Assert(qe != nullptr);
+ Assert(tds != nullptr);
Trace("sygus-red") << "Compute redundant cons for " << tn << std::endl;
d_type = tn;
Assert(tn.isDatatype());
- TermDbSygus* tds = qe->getTermDatabaseSygus();
tds->registerSygusType(tn);
const DType& dt = tn.getDType();
Assert(dt.isSygus());
namespace CVC4 {
namespace theory {
-
-class QuantifiersEngine;
-
namespace quantifiers {
class TermDbSygus;
* qe : pointer to the quantifiers engine,
* tn : the (sygus) type to compute redundant constructors for
*/
- void initialize(QuantifiersEngine* qe, TypeNode tn);
+ void initialize(TermDbSygus* tds, TypeNode tn);
/** Get the indices of the redundant constructors of the register type */
void getRedundant(std::vector<unsigned>& indices);
/**
d_ceg_si(new CegSingleInv(qe)),
d_templInfer(new SygusTemplateInfer),
d_ceg_proc(new SynthConjectureProcess(qe)),
- d_ceg_gc(new CegGrammarConstructor(qe, this)),
+ d_ceg_gc(new CegGrammarConstructor(d_tds, this)),
d_sygus_rconst(new SygusRepairConst(qe)),
d_exampleInfer(new ExampleInfer(d_tds)),
d_ceg_pbe(new SygusPbe(qe, this)),
if( k==DIVISION || k==DIVISION_TOTAL || k==INTS_DIVISION || k==INTS_DIVISION_TOTAL ||
k==INTS_MODULUS || k==INTS_MODULUS_TOTAL ){
if( n[1].isConst() ){
- if (n[1]
- == d_quantEngine->getTermUtil()->getTypeValue(n[1].getType(), 0))
+ if (n[1] == TermUtil::mkTypeValue(n[1].getType(), 0))
{
return true;
}
namespace theory {
namespace quantifiers {
-TermUtil::TermUtil()
-{
- d_true = NodeManager::currentNM()->mkConst(true);
- d_false = NodeManager::currentNM()->mkConst(false);
- d_zero = NodeManager::currentNM()->mkConst(Rational(0));
- d_one = NodeManager::currentNM()->mkConst(Rational(1));
-}
-
-TermUtil::~TermUtil(){
-
-}
-
size_t TermUtil::getVariableNum(Node q, Node v)
{
Node::iterator it = std::find(q[0].begin(), q[0].end(), v);
( n.getKind()!=ITE || n.getType().isBoolean() );
}
-Node TermUtil::getTypeValue(TypeNode tn, int val)
-{
- std::unordered_map<int, Node>::iterator it = d_type_value[tn].find(val);
- if (it == d_type_value[tn].end())
- {
- Node n = mkTypeValue(tn, val);
- d_type_value[tn][val] = n;
- return n;
- }
- return it->second;
-}
-
-Node TermUtil::mkTypeValue(TypeNode tn, int val)
+Node TermUtil::mkTypeValue(TypeNode tn, int32_t val)
{
Node n;
if (tn.isInteger() || tn.isReal())
}
else if (tn.isBitVector())
{
- unsigned int uv = val;
+ // cast to unsigned
+ uint32_t uv = static_cast<uint32_t>(val);
BitVector bval(tn.getConst<BitVectorSize>(), uv);
n = NodeManager::currentNM()->mkConst<BitVector>(bval);
}
return n;
}
-Node TermUtil::getTypeMaxValue(TypeNode tn)
-{
- std::unordered_map<TypeNode, Node, TypeNodeHashFunction>::iterator it =
- d_type_max_value.find(tn);
- if (it == d_type_max_value.end())
- {
- Node n = mkTypeMaxValue(tn);
- d_type_max_value[tn] = n;
- return n;
- }
- return it->second;
-}
-
Node TermUtil::mkTypeMaxValue(TypeNode tn)
{
Node n;
return n;
}
-Node TermUtil::getTypeValueOffset(TypeNode tn,
- Node val,
- int offset,
- int& status)
+Node TermUtil::mkTypeValueOffset(TypeNode tn,
+ Node val,
+ int32_t offset,
+ int32_t& status)
{
- std::unordered_map<int, Node>::iterator it =
- d_type_value_offset[tn][val].find(offset);
- if (it == d_type_value_offset[tn][val].end())
+ Node val_o;
+ Node offset_val = mkTypeValue(tn, offset);
+ status = -1;
+ if (!offset_val.isNull())
{
- Node val_o;
- Node offset_val = getTypeValue(tn, offset);
- status = -1;
- if (!offset_val.isNull())
+ if (tn.isInteger() || tn.isReal())
{
- if (tn.isInteger() || tn.isReal())
- {
- val_o = Rewriter::rewrite(
- NodeManager::currentNM()->mkNode(PLUS, val, offset_val));
- status = 0;
- }
- else if (tn.isBitVector())
- {
- val_o = Rewriter::rewrite(
- NodeManager::currentNM()->mkNode(BITVECTOR_PLUS, val, offset_val));
- // TODO : enable? watch for overflows
- }
+ val_o = Rewriter::rewrite(
+ NodeManager::currentNM()->mkNode(PLUS, val, offset_val));
+ status = 0;
+ }
+ else if (tn.isBitVector())
+ {
+ val_o = Rewriter::rewrite(
+ NodeManager::currentNM()->mkNode(BITVECTOR_PLUS, val, offset_val));
}
- d_type_value_offset[tn][val][offset] = val_o;
- d_type_value_offset_status[tn][val][offset] = status;
- return val_o;
}
- status = d_type_value_offset_status[tn][val][offset];
- return it->second;
+ return val_o;
}
Node TermUtil::mkTypeConst(TypeNode tn, bool pol)
// Assert( ik!=DIVISION && ik!=INTS_DIVISION && ik!=INTS_MODULUS &&
// ik!=BITVECTOR_UDIV );
TypeNode tn = n.getType();
- if (n == getTypeValue(tn, 0))
+ if (n == mkTypeValue(tn, 0))
{
if (ik == PLUS || ik == OR || ik == XOR || ik == BITVECTOR_PLUS
|| ik == BITVECTOR_OR
return arg == 1;
}
}
- else if (n == getTypeValue(tn, 1))
+ else if (n == mkTypeValue(tn, 1))
{
if (ik == MULT || ik == BITVECTOR_MULT)
{
return arg == 1;
}
}
- else if (n == getTypeMaxValue(tn))
+ else if (n == mkTypeMaxValue(tn))
{
if (ik == EQUAL || ik == BITVECTOR_AND || ik == BITVECTOR_XNOR)
{
Node TermUtil::isSingularArg(Node n, Kind ik, unsigned arg)
{
TypeNode tn = n.getType();
- if (n == getTypeValue(tn, 0))
+ if (n == mkTypeValue(tn, 0))
{
if (ik == AND || ik == MULT || ik == BITVECTOR_AND || ik == BITVECTOR_MULT)
{
}
else if (arg == 1)
{
- return getTypeMaxValue(tn);
+ return mkTypeMaxValue(tn);
}
}
else if (ik == DIVISION || ik == DIVISION_TOTAL || ik == INTS_DIVISION
}
else if (arg == 2)
{
- return getTypeValue(NodeManager::currentNM()->stringType(), 0);
+ return mkTypeValue(NodeManager::currentNM()->stringType(), 0);
}
}
else if (ik == STRING_STRIDOF)
{
if (arg == 0 || arg == 1)
{
- return getTypeValue(NodeManager::currentNM()->integerType(), -1);
+ return mkTypeValue(NodeManager::currentNM()->integerType(), -1);
}
}
}
- else if (n == getTypeValue(tn, 1))
+ else if (n == mkTypeValue(tn, 1))
{
if (ik == BITVECTOR_UREM_TOTAL)
{
- return getTypeValue(tn, 0);
+ return mkTypeValue(tn, 0);
}
}
- else if (n == getTypeMaxValue(tn))
+ else if (n == mkTypeMaxValue(tn))
{
if (ik == OR || ik == BITVECTOR_OR)
{
// negative arguments
if (ik == STRING_SUBSTR || ik == STRING_CHARAT)
{
- return getTypeValue(NodeManager::currentNM()->stringType(), 0);
+ return mkTypeValue(NodeManager::currentNM()->stringType(), 0);
}
else if (ik == STRING_STRIDOF)
{
Assert(arg == 2);
- return getTypeValue(NodeManager::currentNM()->integerType(), -1);
+ return mkTypeValue(NodeManager::currentNM()->integerType(), -1);
}
}
}
#include <unordered_set>
#include "expr/attribute.h"
-#include "theory/type_enumerator.h"
+#include "expr/node.h"
namespace CVC4 {
namespace theory {
struct QuantIdNumAttributeId {};
typedef expr::Attribute< QuantIdNumAttributeId, uint64_t > QuantIdNumAttribute;
-class QuantifiersEngine;
-
-namespace inst{
- class Trigger;
- class HigherOrderTrigger;
-}
-
namespace quantifiers {
class TermDatabase;
class TermUtil
{
public:
- TermUtil();
- ~TermUtil();
- /** boolean terms */
- Node d_true;
- Node d_false;
- /** constants */
- Node d_zero;
- Node d_one;
+ TermUtil() {}
+ ~TermUtil() {}
// for inst constant
public:
Node n,
std::vector<Node>& vars);
-public:
-
-//general utilities
- // TODO #1216 : promote these?
- private:
- /** cache for getTypeValue */
- std::unordered_map<TypeNode,
- std::unordered_map<int, Node>,
- TypeNodeHashFunction>
- d_type_value;
- /** cache for getTypeMaxValue */
- std::unordered_map<TypeNode, Node, TypeNodeHashFunction> d_type_max_value;
- /** cache for getTypeValueOffset */
- std::unordered_map<TypeNode,
- std::unordered_map<Node,
- std::unordered_map<int, Node>,
- NodeHashFunction>,
- TypeNodeHashFunction>
- d_type_value_offset;
- /** cache for status of getTypeValueOffset*/
- std::unordered_map<TypeNode,
- std::unordered_map<Node,
- std::unordered_map<int, int>,
- NodeHashFunction>,
- TypeNodeHashFunction>
- d_type_value_offset_status;
-
public:
/** contains uninterpreted constant */
static bool containsUninterpretedConstant( Node n );
* <k>( ... t_{arg-1}, t_{arg+1}...)
* always holds.
*/
- bool isIdempotentArg(Node n, Kind ik, int arg);
+ static bool isIdempotentArg(Node n, Kind ik, int arg);
/** is singular arg
* Returns true if
* <k>( ... t_{arg-1}, n, t_{arg+1}...) = ret
* always holds for some constant ret, which is returned by this function.
*/
- Node isSingularArg(Node n, Kind ik, unsigned arg);
+ static Node isSingularArg(Node n, Kind ik, unsigned arg);
- /** get type value
+ /** get type value with simple value
* This gets the Node that represents value val for Type tn
* This is used to get simple values, e.g. -1,0,1,
* in a uniform way per type.
*/
- Node getTypeValue(TypeNode tn, int val);
-
- /** get type value offset
+ static Node mkTypeValue(TypeNode tn, int32_t val);
+ /** make type value with simple offset
* Returns the value of ( val + getTypeValue( tn, offset ) ),
* where + is the additive operator for the type.
* Stores the status (0: success, -1: failure) in status.
*/
- Node getTypeValueOffset(TypeNode tn, Node val, int offset, int& status);
-
- /** get the "max" value for type tn
+ static Node mkTypeValueOffset(TypeNode tn,
+ Node val,
+ int32_t offset,
+ int32_t& status);
+ /** make the "max" value for type tn
* For example,
* the max value for Bool is true,
* the max value for BitVector is 1..1.
*/
- Node getTypeMaxValue(TypeNode tn);
-
- /** make value, static version of get value */
- static Node mkTypeValue(TypeNode tn, int val);
- /** make value offset, static version of get value offset */
- static Node mkTypeValueOffset(TypeNode tn, Node val, int offset, int& status);
- /** make max value, static version of get max value */
static Node mkTypeMaxValue(TypeNode tn);
/**
* Make const, returns pol ? mkTypeValue(tn,0) : mkTypeMaxValue(tn).
d_tr_trie(new inst::TriggerTrie),
d_model(nullptr),
d_builder(nullptr),
- d_term_util(new quantifiers::TermUtil),
d_term_db(new quantifiers::TermDb(qstate, qim, d_qreg, this)),
d_eq_query(nullptr),
d_sygus_tdb(nullptr),
{
return d_sygus_tdb.get();
}
-quantifiers::TermUtil* QuantifiersEngine::getTermUtil() const
-{
- return d_term_util.get();
-}
quantifiers::QuantAttributes* QuantifiersEngine::getQuantAttributes() const
{
return d_quant_attr.get();
quantifiers::TermDb* getTermDatabase() const;
/** get term database sygus */
quantifiers::TermDbSygus* getTermDatabaseSygus() const;
- /** get term utilities */
- quantifiers::TermUtil* getTermUtil() const;
/** get quantifiers attributes */
quantifiers::QuantAttributes* getQuantAttributes() const;
/** get instantiate utility */
std::unique_ptr<quantifiers::FirstOrderModel> d_model;
/** model builder */
std::unique_ptr<quantifiers::QModelBuilder> d_builder;
- /** term utilities */
- std::unique_ptr<quantifiers::TermUtil> d_term_util;
/** term database */
std::unique_ptr<quantifiers::TermDb> d_term_db;
/** equality query class */
projects / cvc5.git / commitdiff