return out << "index_" << dic.getIndex();
}
+
std::string Datatype::getName() const
{
ExprManagerScope ems(*d_em);
for(std::vector<Datatype>::iterator i = datatypes.begin(), i_end = datatypes.end(); i != i_end; ++i) {
dt_copies.push_back( new Datatype( *i ) );
}
-
+
// First do some sanity checks, set up the final Type to be used for
// each datatype, and set up the "named resolutions" used to handle
// simple self- and mutual-recursion, for example in the definition
#include "theory/datatypes/datatypes_rewriter.h"
+#include "expr/dtype.h"
#include "expr/node_algorithm.h"
#include "expr/sygus_datatype.h"
#include "options/datatypes_options.h"
}
TNode constructor = in[0].getOperator();
size_t constructorIndex = utils::indexOf(constructor);
- const Datatype& dt = Datatype::datatypeOf(constructor.toExpr());
- const DatatypeConstructor& c = dt[constructorIndex];
+ const DType& dt = utils::datatypeOf(constructor);
+ const DTypeConstructor& c = dt[constructorIndex];
unsigned weight = c.getWeight();
children.push_back(nm->mkConst(Rational(weight)));
Node res =
std::vector<Node> cases;
std::vector<Node> rets;
TypeNode t = h.getType();
- const Datatype& dt = t.getDatatype();
+ const DType& dt = t.getDType();
for (size_t k = 1, nchild = in.getNumChildren(); k < nchild; k++)
{
Node c = in[k];
// cons is null in the default case
if (!cons.isNull())
{
- cindex = Datatype::indexOf(cons.toExpr());
+ cindex = utils::indexOf(cons);
}
Node body;
if (ck == MATCH_CASE)
{
vars.push_back(c[0][i]);
Node sc = nm->mkNode(
- APPLY_SELECTOR_TOTAL,
- Node::fromExpr(dt[cindex].getSelectorInternal(t.toType(), i)),
- h);
+ APPLY_SELECTOR_TOTAL, dt[cindex].getSelectorInternal(t, i), h);
subs.push_back(sc);
}
}
if (in.getKind() == kind::APPLY_CONSTRUCTOR)
{
TypeNode tn = in.getType();
- Type t = tn.toType();
- DatatypeType dt = DatatypeType(t);
// check for parametric datatype constructors
// to ensure a normal form, all parameteric datatype constructors must have
// a type ascription
- if (dt.isParametric())
+ if (tn.isParametricDatatype())
{
if (in.getOperator().getKind() != kind::APPLY_TYPE_ASCRIPTION)
{
<< std::endl;
Node op = in.getOperator();
// get the constructor object
- const DatatypeConstructor& dtc =
- Datatype::datatypeOf(op.toExpr())[utils::indexOf(op)];
+ const DTypeConstructor& dtc = utils::datatypeOf(op)[utils::indexOf(op)];
// create ascribed constructor type
Node tc = NodeManager::currentNM()->mkConst(
- AscriptionType(dtc.getSpecializedConstructorType(t)));
+ AscriptionType(dtc.getSpecializedConstructorType(tn).toType()));
Node op_new = NodeManager::currentNM()->mkNode(
kind::APPLY_TYPE_ASCRIPTION, tc, op);
// make new node
// e.g. "pred(zero)".
TypeNode tn = in.getType();
TypeNode argType = in[0].getType();
- Expr selector = in.getOperator().toExpr();
+ Node selector = in.getOperator();
TNode constructor = in[0].getOperator();
size_t constructorIndex = utils::indexOf(constructor);
- const Datatype& dt = Datatype::datatypeOf(selector);
- const DatatypeConstructor& c = dt[constructorIndex];
+ const DType& dt = utils::datatypeOf(selector);
+ const DTypeConstructor& c = dt[constructorIndex];
Trace("datatypes-rewrite-debug") << "Rewriting collapsable selector : "
<< in;
Trace("datatypes-rewrite-debug") << ", cindex = " << constructorIndex
// The argument index of external selectors (applications of
// APPLY_SELECTOR) is given by an attribute and obtained via indexOf below
// The argument is only valid if it is the proper constructor.
- selectorIndex = Datatype::indexOf(selector);
+ selectorIndex = utils::indexOf(selector);
if (selectorIndex < 0
|| selectorIndex >= static_cast<int>(c.getNumArgs()))
{
//}
if (tn.isDatatype())
{
- const Datatype& dta = ((DatatypeType)(tn).toType()).getDatatype();
+ const DType& dta = tn.getDType();
useTe = !dta.isCodatatype();
}
if (useTe)
return RewriteResponse(REWRITE_DONE,
NodeManager::currentNM()->mkConst(result));
}
- const Datatype& dt = static_cast<DatatypeType>(in[0].getType().toType()).getDatatype();
+ const DType& dt = in[0].getType().getDType();
if (dt.getNumConstructors() == 1 && !dt.isSygus())
{
// only one constructor, so it must be
#include "theory/datatypes/sygus_extension.h"
+#include "expr/dtype.h"
#include "expr/node_manager.h"
#include "expr/sygus_datatype.h"
#include "options/base_options.h"
Assert(itt != d_testers.end());
int ptindex = (*itt).second;
TypeNode ptn = n[0].getType();
- const Datatype& pdt = ((DatatypeType)ptn.toType()).getDatatype();
- int sindex_in_parent = pdt[ptindex].getSelectorIndexInternal( n.getOperator().toExpr() );
+ const DType& pdt = ptn.getDType();
+ int sindex_in_parent =
+ pdt[ptindex].getSelectorIndexInternal(n.getOperator());
// the tester is irrelevant in this branch
if( sindex_in_parent==-1 ){
do_add = false;
sz_eq_cases.push_back( sz_eq );
if( options::sygusOpt1() ){
TypeNode tnc = n1.getType();
- const Datatype& cdt = ((DatatypeType)(tnc).toType()).getDatatype();
+ const DType& cdt = tnc.getDType();
for( unsigned j=0; j<cdt.getNumConstructors(); j++ ){
std::vector<Node> case_conj;
for (unsigned k = 0; k < j; k++)
}
}
if( success ){
- Trace("sygus-sb-debug") << "Register : " << n << ", depth : " << d << ", top level = " << is_top_level << ", type = " << ((DatatypeType)tn.toType()).getDatatype().getName() << std::endl;
+ Trace("sygus-sb-debug")
+ << "Register : " << n << ", depth : " << d
+ << ", top level = " << is_top_level
+ << ", type = " << tn.getDType().getName() << std::endl;
d_term_to_depth[n] = d;
d_is_top_level[n] = is_top_level;
registerSearchTerm( tn, d, n, is_top_level, lemmas );
// nothing to do for non-datatype types
return;
}
- const Datatype& dt = static_cast<DatatypeType>(ntn.toType()).getDatatype();
+ const DType& dt = ntn.getDType();
if (!dt.isSygus())
{
// nothing to do for non-sygus-datatype type
IntMap::const_iterator ittv = d_testers.find( x );
Assert(ittv != d_testers.end());
int tindex = (*ittv).second;
- const Datatype& dti = ((DatatypeType)x.getType().toType()).getDatatype();
+ const DType& dti = x.getType().getDType();
if( dti[tindex].getNumArgs()>0 ){
NodeMap::const_iterator itt = d_testers_exp.find( x );
Assert(itt != d_testers_exp.end());
if( options::sygusSymBreakLazy() ){
Trace("sygus-sb-debug") << "Do lazy symmetry breaking...\n";
for( unsigned j=0; j<dt[tindex].getNumArgs(); j++ ){
- Node sel = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[tindex].getSelectorInternal( ntn.toType(), j ) ), n );
+ Node sel = nm->mkNode(
+ APPLY_SELECTOR_TOTAL, dt[tindex].getSelectorInternal(ntn, j), n);
Trace("sygus-sb-debug2") << " activate child sel : " << sel << std::endl;
Assert(d_active_terms.find(sel) == d_active_terms.end());
IntMap::const_iterator itt = d_testers.find( sel );
Node cond;
if( n.getKind()==APPLY_SELECTOR_TOTAL && options::sygusSymBreakRlv() ){
TypeNode ntn = n[0].getType();
- Type nt = ntn.toType();
- const Datatype& dt = ((DatatypeType)nt).getDatatype();
- Expr selExpr = n.getOperator().toExpr();
+ const DType& dt = ntn.getDType();
+ Node sel = n.getOperator();
if( options::dtSharedSelectors() ){
std::vector< Node > disj;
bool excl = false;
for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
- int sindexi = dt[i].getSelectorIndexInternal(selExpr);
+ int sindexi = dt[i].getSelectorIndexInternal(sel);
if (sindexi != -1)
{
disj.push_back(utils::mkTester(n[0], i, dt).negate());
kind::AND, disj);
}
}else{
- int sindex = Datatype::cindexOf( selExpr );
+ int sindex = utils::cindexOf(sel);
Assert(sindex != -1);
cond = utils::mkTester(n[0], sindex, dt).negate();
}
Assert(tn.isDatatype());
NodeManager* nm = NodeManager::currentNM();
Node n = getFreeVar(tn);
- const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+ const DType& dt = tn.getDType();
Assert(dt.isSygus());
Assert(tindex >= 0 && tindex < static_cast<int>(dt.getNumConstructors()));
quantifiers::SygusTypeInfo& ti = d_tds->getTypeInfo(tn);
// get the sygus operator
- Node sop = Node::fromExpr(dt[tindex].getSygusOp());
+ Node sop = dt[tindex].getSygusOp();
// get the kind of the constructor operator
Kind nk = ti.getConsNumKind(tindex);
// is this the any-constant constructor?
unsigned dt_index_nargs = isAnyConstant ? 0 : dt[tindex].getNumArgs();
// builtin type
- TypeNode tnb = TypeNode::fromType(dt.getSygusType());
+ TypeNode tnb = dt.getSygusType();
// get children
std::vector<Node> children;
for (unsigned j = 0; j < dt_index_nargs; j++)
{
Node sel = nm->mkNode(
- APPLY_SELECTOR_TOTAL,
- Node::fromExpr(dt[tindex].getSelectorInternal(tn.toType(), j)),
- n);
+ APPLY_SELECTOR_TOTAL, dt[tindex].getSelectorInternal(tn, j), n);
Assert(sel.getType().isDatatype());
children.push_back(sel);
}
// is the tindex^{th} constructor of dt. Thus, is-x_i( z ) is either
// true or false below.
- Node svl = Node::fromExpr(dt.getSygusVarList());
+ Node svl = dt.getSygusVarList();
// for each variable
Assert(!e.isNull());
TypeNode etn = e.getType();
{
children_solved[j] = i;
TypeNode ctn = children[j].getType();
- const Datatype& cdt =
- static_cast<DatatypeType>(ctn.toType()).getDatatype();
+ const DType& cdt = ctn.getDType();
Assert(i < static_cast<int>(cdt.getNumConstructors()));
sbp_conj.push_back(utils::mkTester(children[j], i, cdt));
}
TypeNode tnc = nc.getType();
quantifiers::SygusTypeInfo& cti = d_tds->getTypeInfo(tnc);
int anyc_cons_num = cti.getAnyConstantConsNum();
- const Datatype& cdt =
- static_cast<DatatypeType>(tnc.toType()).getDatatype();
+ const DType& cdt = tnc.getDType();
std::vector<Node> exp_const;
for (unsigned k = 0, ncons = cdt.getNumConstructors(); k < ncons; k++)
{
&& children[0].getType() == tn && children[1].getType() == tn)
{
// chainable
- Node child11 = nm->mkNode(
- APPLY_SELECTOR_TOTAL,
- Node::fromExpr(dt[tindex].getSelectorInternal(tn.toType(), 1)),
- children[0]);
+ Node child11 = nm->mkNode(APPLY_SELECTOR_TOTAL,
+ dt[tindex].getSelectorInternal(tn, 1),
+ children[0]);
Assert(child11.getType() == children[1].getType());
Node order_pred_trans =
nm->mkNode(OR,
// selector chain n.
return n;
}
- const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype();
+ const DType& dt = tn.getDType();
if (!dt.isSygus())
{
// don't register non-sygus-datatype terms
for (unsigned i = 0, nchild = nv.getNumChildren(); i < nchild; i++)
{
Node sel = nm->mkNode(
- APPLY_SELECTOR_TOTAL,
- Node::fromExpr(dt[cindex].getSelectorInternal(tn.toType(), i)),
- n);
+ APPLY_SELECTOR_TOTAL, dt[cindex].getSelectorInternal(tn, i), n);
Node nvc = registerSearchValue(a,
sel,
nv[i],
d_register_st[e] = false;
return;
}
- const Datatype& dt = etn.getDatatype();
+ const DType& dt = etn.getDType();
if (!dt.isSygus())
{
// not a sygus datatype term
{
// if it is variable agnostic, enforce top-level constraint that says no
// variables occur pre-traversal at top-level
- Node varList = Node::fromExpr(dt.getSygusVarList());
+ Node varList = dt.getSygusVarList();
std::vector<Node> constraints;
quantifiers::SygusTypeInfo& eti = d_tds->getTypeInfo(etn);
for (const Node& v : varList)
<< std::endl;
}
TypeNode tn = n.getType();
- const Datatype& dt = tn.getDatatype();
+ const DType& dt = tn.getDType();
Assert(dt.isSygus());
// ensure that the expected size bound is met
}
for( unsigned i=0; i<vn.getNumChildren(); i++ ){
Node sel = nm->mkNode(
- APPLY_SELECTOR_TOTAL,
- Node::fromExpr(dt[cindex].getSelectorInternal(tn.toType(), i)),
- n);
+ APPLY_SELECTOR_TOTAL, dt[cindex].getSelectorInternal(tn, i), n);
if (!checkValue(sel, vn[i], ind + 1, lemmas))
{
return false;
TypeNode tn = n.getType();
IntMap::const_iterator it = d_testers.find( n );
Assert(it != d_testers.end());
- const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype();
+ const DType& dt = tn.getDType();
int tindex = (*it).second;
Assert(tindex >= 0);
Assert(tindex < (int)dt.getNumConstructors());
std::vector< Node > children;
- children.push_back( Node::fromExpr( dt[tindex].getConstructor() ) );
+ children.push_back(dt[tindex].getConstructor());
for( unsigned i=0; i<dt[tindex].getNumArgs(); i++ ){
- Node sel = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[tindex].getSelectorInternal( tn.toType(), i ) ), n );
+ Node sel = NodeManager::currentNM()->mkNode(
+ APPLY_SELECTOR_TOTAL, dt[tindex].getSelectorInternal(tn, i), n);
Node cc = getCurrentTemplate( sel, var_count );
children.push_back( cc );
}
bool SygusSimpleSymBreak::considerArgKind(
TypeNode tn, TypeNode tnp, Kind k, Kind pk, int arg)
{
- const Datatype& pdt = ((DatatypeType)(tnp).toType()).getDatatype();
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ const DType& pdt = tnp.getDType();
+ const DType& dt = tn.getDType();
quantifiers::SygusTypeInfo& ti = d_tds->getTypeInfo(tn);
quantifiers::SygusTypeInfo& pti = d_tds->getTypeInfo(tnp);
Assert(ti.hasKind(k));
// the argument types of the child must be the parent's type
for (unsigned i = 0, nargs = dt[c].getNumArgs(); i < nargs; i++)
{
- TypeNode tn = TypeNode::fromType(dt[c].getArgType(i));
+ TypeNode tn = dt[c].getArgType(i);
if (tn != tnp)
{
return true;
// negation normal form
if (pk == k)
{
- rt.d_req_type = TypeNode::fromType(dt[c].getArgType(0));
+ rt.d_req_type = dt[c].getArgType(0);
}
else
{
rt.d_req_kind = ITE;
reqkc[1] = NOT;
reqkc[2] = NOT;
- rt.d_children[0].d_req_type = TypeNode::fromType(dt[c].getArgType(0));
+ rt.d_children[0].d_req_type = dt[c].getArgType(0);
}
else if (k == LEQ || k == GT)
{
// (not (~ x y)) -----> (~ (+ y 1) x)
rt.d_req_kind = k;
rt.d_children[0].d_req_kind = PLUS;
- rt.d_children[0].d_children[0].d_req_type =
- TypeNode::fromType(dt[c].getArgType(1));
+ rt.d_children[0].d_children[0].d_req_type = dt[c].getArgType(1);
rt.d_children[0].d_children[1].d_req_const =
NodeManager::currentNM()->mkConst(Rational(1));
- rt.d_children[1].d_req_type = TypeNode::fromType(dt[c].getArgType(0));
+ rt.d_children[1].d_req_type = dt[c].getArgType(0);
}
else if (k == LT || k == GEQ)
{
// (not (~ x y)) -----> (~ y (+ x 1))
rt.d_req_kind = k;
- rt.d_children[0].d_req_type = TypeNode::fromType(dt[c].getArgType(1));
+ rt.d_children[0].d_req_type = dt[c].getArgType(1);
rt.d_children[1].d_req_kind = PLUS;
- rt.d_children[1].d_children[0].d_req_type =
- TypeNode::fromType(dt[c].getArgType(0));
+ rt.d_children[1].d_children[0].d_req_type = dt[c].getArgType(0);
rt.d_children[1].d_children[1].d_req_const =
NodeManager::currentNM()->mkConst(Rational(1));
}
if (rk != UNDEFINED_KIND)
{
rt.d_children[i].d_req_kind = rk;
- rt.d_children[i].d_children[0].d_req_type =
- TypeNode::fromType(dt[c].getArgType(i));
+ rt.d_children[i].d_children[0].d_req_type = dt[c].getArgType(i);
}
}
}
// (~ x (- y z)) ----> (~ (+ x z) y)
// (~ (- y z) x) ----> (~ y (+ x z))
rt.d_req_kind = pk;
- rt.d_children[arg].d_req_type = TypeNode::fromType(dt[c].getArgType(0));
+ rt.d_children[arg].d_req_type = dt[c].getArgType(0);
rt.d_children[oarg].d_req_kind = k == MINUS ? PLUS : BITVECTOR_PLUS;
- rt.d_children[oarg].d_children[0].d_req_type =
- TypeNode::fromType(pdt[pc].getArgType(oarg));
- rt.d_children[oarg].d_children[1].d_req_type =
- TypeNode::fromType(dt[c].getArgType(1));
+ rt.d_children[oarg].d_children[0].d_req_type = pdt[pc].getArgType(oarg);
+ rt.d_children[oarg].d_children[1].d_req_type = dt[c].getArgType(1);
}
else if (pk == PLUS || pk == BITVECTOR_PLUS)
{
rt.d_req_kind = pk == PLUS ? MINUS : BITVECTOR_SUB;
int oarg = arg == 0 ? 1 : 0;
rt.d_children[0].d_req_kind = pk;
- rt.d_children[0].d_children[0].d_req_type =
- TypeNode::fromType(pdt[pc].getArgType(oarg));
- rt.d_children[0].d_children[1].d_req_type =
- TypeNode::fromType(dt[c].getArgType(0));
- rt.d_children[1].d_req_type = TypeNode::fromType(dt[c].getArgType(1));
+ rt.d_children[0].d_children[0].d_req_type = pdt[pc].getArgType(oarg);
+ rt.d_children[0].d_children[1].d_req_type = dt[c].getArgType(0);
+ rt.d_children[1].d_req_type = dt[c].getArgType(1);
}
}
else if (k == ITE)
{
// (o X (ite y z w) X') -----> (ite y (o X z X') (o X w X'))
rt.d_req_kind = ITE;
- rt.d_children[0].d_req_type = TypeNode::fromType(dt[c].getArgType(0));
+ rt.d_children[0].d_req_type = dt[c].getArgType(0);
unsigned n_args = pdt[pc].getNumArgs();
for (unsigned r = 1; r <= 2; r++)
{
{
if ((int)q == arg)
{
- rt.d_children[r].d_children[q].d_req_type =
- TypeNode::fromType(dt[c].getArgType(r));
+ rt.d_children[r].d_children[q].d_req_type = dt[c].getArgType(r);
}
else
{
- rt.d_children[r].d_children[q].d_req_type =
- TypeNode::fromType(pdt[pc].getArgType(q));
+ rt.d_children[r].d_children[q].d_req_type = pdt[pc].getArgType(q);
}
}
}
{
// (ite (not y) z w) -----> (ite y w z)
rt.d_req_kind = ITE;
- rt.d_children[0].d_req_type = TypeNode::fromType(dt[c].getArgType(0));
- rt.d_children[1].d_req_type = TypeNode::fromType(pdt[pc].getArgType(2));
- rt.d_children[2].d_req_type = TypeNode::fromType(pdt[pc].getArgType(1));
+ rt.d_children[0].d_req_type = dt[c].getArgType(0);
+ rt.d_children[1].d_req_type = pdt[pc].getArgType(2);
+ rt.d_children[2].d_req_type = pdt[pc].getArgType(1);
}
}
Trace("sygus-sb-debug") << "Consider sygus arg kind " << k << ", pk = " << pk
bool SygusSimpleSymBreak::considerConst(
TypeNode tn, TypeNode tnp, Node c, Kind pk, int arg)
{
- const Datatype& pdt = static_cast<DatatypeType>(tnp.toType()).getDatatype();
+ const DType& pdt = tnp.getDType();
// child grammar-independent
if (!considerConst(pdt, tnp, c, pk, arg))
{
}
bool SygusSimpleSymBreak::considerConst(
- const Datatype& pdt, TypeNode tnp, Node c, Kind pk, int arg)
+ const DType& pdt, TypeNode tnp, Node c, Kind pk, int arg)
{
quantifiers::SygusTypeInfo& pti = d_tds->getTypeInfo(tnp);
Assert(pti.hasKind(pk));
if (pdt[pc].getNumArgs() == 2)
{
int oarg = arg == 0 ? 1 : 0;
- TypeNode otn = TypeNode::fromType(pdt[pc].getArgType(oarg));
+ TypeNode otn = pdt[pc].getArgType(oarg);
if (otn == tnp)
{
Trace("sygus-sb-simple")
if (c == one_c && arg == 2)
{
rt.d_req_kind = STRING_CHARAT;
- rt.d_children[0].d_req_type = TypeNode::fromType(pdt[pc].getArgType(0));
- rt.d_children[1].d_req_type = TypeNode::fromType(pdt[pc].getArgType(1));
+ rt.d_children[0].d_req_type = pdt[pc].getArgType(0);
+ rt.d_children[1].d_req_type = pdt[pc].getArgType(1);
}
}
if (!rt.empty())
return -1;
}
-int SygusSimpleSymBreak::getFirstArgOccurrence(const DatatypeConstructor& c,
+int SygusSimpleSymBreak::getFirstArgOccurrence(const DTypeConstructor& c,
TypeNode tn)
{
for (unsigned i = 0, nargs = c.getNumArgs(); i < nargs; i++)
{
- TypeNode tni = TypeNode::fromType(c.getArgType(i));
- if (tni == tn)
+ if (c.getArgType(i) == tn)
{
return i;
}
#define CVC4__THEORY__DATATYPES__SIMPLE_SYM_BREAK_H
#include <map>
+#include "expr/dtype.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
/** 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 DatatypeConstructor& c, TypeNode tn);
+ int getFirstArgOccurrence(const DTypeConstructor& c, TypeNode tn);
/**
* Helper function for consider const above, pdt is the datatype of the type
* of tnp.
*/
- bool considerConst(
- const Datatype& pdt, TypeNode tnp, Node c, Kind pk, int arg);
+ bool considerConst(const DType& pdt, TypeNode tnp, Node c, Kind pk, int arg);
};
} // namespace datatypes
#include "base/check.h"
#include "expr/datatype.h"
+#include "expr/dtype.h"
#include "expr/kind.h"
#include "options/datatypes_options.h"
#include "options/quantifiers_options.h"
//if there are more than 1 possible constructors for eqc
if( !hasLabel( eqc, n ) ){
Trace("datatypes-debug") << "No constructor..." << std::endl;
- Type tt = tn.toType();
- const Datatype& dt = ((DatatypeType)tt).getDatatype();
+ TypeNode tt = tn;
+ const DType& dt = tt.getDType();
Trace("datatypes-debug")
- << "Datatype " << dt << " is " << dt.isInterpretedFinite(tt)
- << " " << dt.isRecursiveSingleton(tt) << std::endl;
+ << "Datatype " << dt.getName() << " is "
+ << dt.isInterpretedFinite(tt) << " "
+ << dt.isRecursiveSingleton(tt) << std::endl;
bool continueProc = true;
if( dt.isRecursiveSingleton( tt ) ){
Trace("datatypes-debug") << "Check recursive singleton..." << std::endl;
//otherwise, if the logic is quantified, under the assumption that all uninterpreted sorts have cardinality one,
// infer the equality.
for( unsigned i=0; i<dt.getNumRecursiveSingletonArgTypes( tt ); i++ ){
- TypeNode tn = TypeNode::fromType( dt.getRecursiveSingletonArgType( tt, i ) );
+ TypeNode tn = dt.getRecursiveSingletonArgType(tt, i);
if( getQuantifiersEngine() ){
// under the assumption that the cardinality of this type is one
Node a = getSingletonLemma( tn, true );
{
Trace("dt-expand") << "Dt Expand definition : " << n << std::endl;
Node selector = n.getOperator();
- Expr selectorExpr = selector.toExpr();
// APPLY_SELECTOR always applies to an external selector, cindexOf is
// legal here
- size_t cindex = Datatype::cindexOf(selectorExpr);
- const Datatype& dt = Datatype::datatypeOf(selectorExpr);
- const DatatypeConstructor& c = dt[cindex];
+ size_t cindex = utils::cindexOf(selector);
+ const DType& dt = utils::datatypeOf(selector);
+ const DTypeConstructor& c = dt[cindex];
Node selector_use;
TypeNode ndt = n[0].getType();
if (options::dtSharedSelectors())
Trace("dt-expand") << "...selector index = " << selectorIndex
<< std::endl;
Assert(selectorIndex < c.getNumArgs());
- selector_use =
- Node::fromExpr(c.getSelectorInternal(ndt.toType(), selectorIndex));
+ selector_use = c.getSelectorInternal(ndt, selectorIndex);
}else{
selector_use = selector;
}
}
else
{
- Expr tester = c.getTester();
- Node tst = nm->mkNode(kind::APPLY_TESTER, Node::fromExpr(tester), n[0]);
+ Node tester = c.getTester();
+ Node tst = nm->mkNode(APPLY_TESTER, tester, n[0]);
tst = Rewriter::rewrite(tst);
Node n_ret;
if (tst == d_true)
{
TypeNode t = n.getType();
Assert(t.isDatatype());
- const Datatype& dt = DatatypeType(t.toType()).getDatatype();
+ const DType& dt = t.getDType();
NodeBuilder<> b(APPLY_CONSTRUCTOR);
- b << Node::fromExpr(dt[0].getConstructor());
+ b << dt[0].getConstructor();
size_t size, updateIndex;
if (n.getKind() == TUPLE_UPDATE)
{
else
{
b << nm->mkNode(
- APPLY_SELECTOR_TOTAL,
- Node::fromExpr(dt[0].getSelectorInternal(t.toType(), i)),
- n[0]);
+ APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal(t, i), n[0]);
Debug("tuprec") << "arg " << i << " copies "
<< b[b.getNumChildren() - 1] << std::endl;
}
void TheoryDatatypes::getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool >& pcons ){
TypeNode tn = n.getType();
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ const DType& dt = tn.getDType();
int lindex = getLabelIndex( eqc, n );
pcons.resize( dt.getNumConstructors(), lindex==-1 );
if( lindex!=-1 ){
d_labels_tindex[n].push_back(ttindex);
}
n_lbl++;
-
- const Datatype& dt = ((DatatypeType)(t_arg.getType()).toType()).getDatatype();
+
+ const DType& dt = t_arg.getType().getDType();
Debug("datatypes-labels") << "Labels at " << n_lbl << " / " << dt.getNumConstructors() << std::endl;
if( tpolarity ){
instantiate( eqc, n );
use_s = s;
}
if( s.getKind()==kind::APPLY_SELECTOR_TOTAL ){
- Expr selectorExpr = s.getOperator().toExpr();
+ Node selector = s.getOperator();
size_t constructorIndex = utils::indexOf(c.getOperator());
- const Datatype& dt = Datatype::datatypeOf(selectorExpr);
- const DatatypeConstructor& dtc = dt[constructorIndex];
- int selectorIndex = dtc.getSelectorIndexInternal( selectorExpr );
+ const DType& dt = utils::datatypeOf(selector);
+ const DTypeConstructor& dtc = dt[constructorIndex];
+ int selectorIndex = dtc.getSelectorIndexInternal(selector);
wrong = selectorIndex<0;
//if( wrong ){
Node eqc = nodes[index];
Node neqc;
bool addCons = false;
- Type tt = eqc.getType().toType();
- const Datatype& dt = ((DatatypeType)tt).getDatatype();
+ TypeNode tt = eqc.getType();
+ const DType& dt = tt.getDType();
if( !d_equalityEngine.hasTerm( eqc ) ){
Assert(false);
}else{
else if (nk == DT_HEIGHT_BOUND && n[1].getConst<Rational>().isZero())
{
std::vector<Node> children;
- const Datatype& dt = n[0].getType().getDatatype();
+ const DType& dt = n[0].getType().getDType();
for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
{
if (utils::isNullaryConstructor(dt[i]))
}
}
-Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index ){
+Node TheoryDatatypes::getInstantiateCons(Node n, const DType& dt, int index)
+{
std::map< int, Node >::iterator it = d_inst_map[n].find( index );
if( it!=d_inst_map[n].end() ){
return it->second;
exp = getLabel(n);
tt = exp[0];
}
- const Datatype& dt = ((DatatypeType)(tt.getType()).toType()).getDatatype();
+ const DType& dt = tt.getType().getDType();
// instantiate this equivalence class
eqc->d_inst = true;
Node tt_cons = getInstantiateCons(tt, dt, index);
if( !tn.isDatatype() ){
addLemma = true;
}else{
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ const DType& dt = tn.getDType();
addLemma = dt.involvesExternalType();
}
}else if( n.getKind()==LEQ || n.getKind()==OR ){
/** collect terms */
void collectTerms( Node n );
/** get instantiate cons */
- Node getInstantiateCons( Node n, const Datatype& dt, int index );
+ Node getInstantiateCons(Node n, const DType& dt, int index);
/** check instantiate */
void instantiate( EqcInfo* eqc, Node n );
/** must communicate fact */
#ifndef CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H
#define CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H
+#include "expr/dtype.h"
#include "expr/type_matcher.h"
#include "theory/datatypes/theory_datatypes_utils.h"
return false;
}
}
- //if we support subtyping for tuples, enable this
- /*
- //check whether it is in normal form?
- TypeNode tn = n.getType();
- if( tn.isTuple() ){
- const Datatype& dt = tn.getDatatype();
- //may be the wrong constructor, if children types are subtypes
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- if( n[i].getType()!=TypeNode::fromType( dt[0][i].getRangeType() ) ){
- return false;
- }
- }
- }else if( tn.isCodatatype() ){
- //TODO?
- }
- */
return true;
}
}; /* struct DatatypeConstructorTypeRule */
throw TypeCheckingExceptionPrivate(
n, "datatype sygus eval takes a datatype head");
}
- const Datatype& dt = headType.getDatatype();
+ const DType& dt = headType.getDType();
if (!dt.isSygus())
{
throw TypeCheckingExceptionPrivate(
}
if (check)
{
- Node svl = Node::fromExpr(dt.getSygusVarList());
+ Node svl = dt.getSygusVarList();
if (svl.getNumChildren() + 1 != n.getNumChildren())
{
throw TypeCheckingExceptionPrivate(n,
}
}
}
- return TypeNode::fromType(dt.getSygusType());
+ return dt.getSygusType();
}
}; /* class DtSyguEvalTypeRule */
{
throw TypeCheckingExceptionPrivate(n, "expecting datatype head in match");
}
- const Datatype& hdt = headType.getDatatype();
+ const DType& hdt = headType.getDType();
std::unordered_set<unsigned> patIndices;
bool patHasVariable = false;
throw TypeCheckingExceptionPrivate(
n, "unexpected kind of term in pattern in match");
}
- const Datatype& pdt = patType.getDatatype();
+ const DType& pdt = patType.getDType();
// compare datatypes instead of the types to catch parametric case,
// where the pattern has parametric type.
- if (hdt != pdt)
+ if (hdt.getTypeNode() != pdt.getTypeNode())
{
std::stringstream ss;
ss << "pattern of a match case does not match the head type in match";
#include "theory/datatypes/theory_datatypes_utils.h"
+#include "expr/dtype.h"
#include "expr/node_algorithm.h"
#include "expr/sygus_datatype.h"
#include "theory/evaluator.h"
namespace datatypes {
namespace utils {
-Node applySygusArgs(const Datatype& dt,
+Node applySygusArgs(const DType& dt,
Node op,
Node n,
const std::vector<Node>& args)
{
Assert(n.hasAttribute(SygusVarNumAttribute()));
int vn = n.getAttribute(SygusVarNumAttribute());
- Assert(Node::fromExpr(dt.getSygusVarList())[vn] == n);
+ Assert(dt.getSygusVarList()[vn] == n);
return args[vn];
}
// n is an application of operator op.
}
// do the full substitution
std::vector<Node> vars;
- Node bvl = Node::fromExpr(dt.getSygusVarList());
+ Node bvl = dt.getSygusVarList();
for (unsigned i = 0, nvars = bvl.getNumChildren(); i < nvars; i++)
{
vars.push_back(bvl[i]);
return UNDEFINED_KIND;
}
-Node mkSygusTerm(const Datatype& dt,
+Node mkSygusTerm(const DType& dt,
unsigned i,
const std::vector<Node>& children,
bool doBetaReduction)
Assert(i < dt.getNumConstructors());
Assert(dt.isSygus());
Assert(!dt[i].getSygusOp().isNull());
- Node op = Node::fromExpr(dt[i].getSygusOp());
+ Node op = dt[i].getSygusOp();
return mkSygusTerm(op, children, doBetaReduction);
}
}
/** get instantiate cons */
-Node getInstCons(Node n, const Datatype& dt, int index)
+Node getInstCons(Node n, const DType& dt, int index)
{
Assert(index >= 0 && index < (int)dt.getNumConstructors());
std::vector<Node> children;
NodeManager* nm = NodeManager::currentNM();
- children.push_back(Node::fromExpr(dt[index].getConstructor()));
- Type t = n.getType().toType();
+ children.push_back(dt[index].getConstructor());
+ TypeNode tn = n.getType();
for (unsigned i = 0, nargs = dt[index].getNumArgs(); i < nargs; i++)
{
- Node nc = nm->mkNode(APPLY_SELECTOR_TOTAL,
- Node::fromExpr(dt[index].getSelectorInternal(t, i)),
- n);
+ Node nc = nm->mkNode(
+ APPLY_SELECTOR_TOTAL, dt[index].getSelectorInternal(tn, i), n);
children.push_back(nc);
}
Node n_ic = nm->mkNode(APPLY_CONSTRUCTOR, children);
if (dt.isParametric())
{
- TypeNode tn = TypeNode::fromType(t);
// add type ascription for ambiguous constructor types
if (!n_ic.getType().isComparableTo(tn))
{
<< n.getType() << std::endl;
Debug("datatypes-parametric")
<< "Constructor is " << dt[index] << std::endl;
- Type tspec =
- dt[index].getSpecializedConstructorType(n.getType().toType());
+ TypeNode tspec = dt[index].getSpecializedConstructorType(n.getType());
Debug("datatypes-parametric")
<< "Type specification is " << tspec << std::endl;
children[0] = nm->mkNode(APPLY_TYPE_ASCRIPTION,
- nm->mkConst(AscriptionType(tspec)),
+ nm->mkConst(AscriptionType(tspec.toType())),
children[0]);
n_ic = nm->mkNode(APPLY_CONSTRUCTOR, children);
Assert(n_ic.getType() == tn);
return n_ic;
}
-int isInstCons(Node t, Node n, const Datatype& dt)
+int isInstCons(Node t, Node n, const DType& dt)
{
if (n.getKind() == APPLY_CONSTRUCTOR)
{
int index = indexOf(n.getOperator());
- const DatatypeConstructor& c = dt[index];
- Type nt = n.getType().toType();
+ const DTypeConstructor& c = dt[index];
+ TypeNode tn = n.getType();
for (unsigned i = 0, size = n.getNumChildren(); i < size; i++)
{
if (n[i].getKind() != APPLY_SELECTOR_TOTAL
- || n[i].getOperator() != Node::fromExpr(c.getSelectorInternal(nt, i))
- || n[i][0] != t)
+ || n[i].getOperator() != c.getSelectorInternal(tn, i) || n[i][0] != t)
{
return -1;
}
return -1;
}
-struct DtIndexAttributeId
-{
-};
-typedef expr::Attribute<DtIndexAttributeId, uint64_t> DtIndexAttribute;
+size_t indexOf(Node n) { return DType::indexOf(n); }
+
+size_t cindexOf(Node n) { return DType::cindexOf(n); }
-unsigned indexOf(Node n)
+const DType& datatypeOf(Node n)
{
- if (!n.hasAttribute(DtIndexAttribute()))
- {
- Assert(n.getType().isConstructor() || n.getType().isTester()
- || n.getType().isSelector());
- unsigned index = Datatype::indexOfInternal(n.toExpr());
- n.setAttribute(DtIndexAttribute(), index);
- return index;
+ TypeNode t = n.getType();
+ switch (t.getKind())
+ {
+ case CONSTRUCTOR_TYPE: return t[t.getNumChildren() - 1].getDType();
+ case SELECTOR_TYPE:
+ case TESTER_TYPE: return t[0].getDType();
+ default:
+ Unhandled() << "arg must be a datatype constructor, selector, or tester";
}
- return n.getAttribute(DtIndexAttribute());
}
-Node mkTester(Node n, int i, const Datatype& dt)
+Node mkTester(Node n, int i, const DType& dt)
{
- return NodeManager::currentNM()->mkNode(
- APPLY_TESTER, Node::fromExpr(dt[i].getTester()), n);
+ return NodeManager::currentNM()->mkNode(APPLY_TESTER, dt[i].getTester(), n);
}
-Node mkSplit(Node n, const Datatype& dt)
+Node mkSplit(Node n, const DType& dt)
{
std::vector<Node> splits;
for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
return true;
}
-bool isNullaryConstructor(const DatatypeConstructor& c)
+bool isNullaryConstructor(const DTypeConstructor& c)
{
for (unsigned j = 0, nargs = c.getNumArgs(); j < nargs; j++)
{
{
Node ret = cur;
Assert(cur.getKind() == APPLY_CONSTRUCTOR);
- const Datatype& dt = cur.getType().getDatatype();
+ const DType& dt = cur.getType().getDType();
// Non sygus-datatype terms are also themselves. Notice we treat the
// case of non-sygus datatypes this way since it avoids computing
// the type / datatype of the node in the pre-traversal above. The
{
Node ret = cur;
Assert(cur.getKind() == APPLY_CONSTRUCTOR);
- const Datatype& dt = cur.getType().getDatatype();
+ const DType& dt = cur.getType().getDType();
// non sygus-datatype terms are also themselves
if (dt.isSygus())
{
#include <vector>
+#include "expr/dtype.h"
#include "expr/node.h"
#include "expr/node_manager_attributes.h"
* This returns the term C( sel^{C,1}( n ), ..., sel^{C,m}( n ) ),
* where C is the index^{th} constructor of datatype dt.
*/
-Node getInstCons(Node n, const Datatype& dt, int index);
+Node getInstCons(Node n, const DType& dt, int index);
/** is instantiation cons
*
* If this method returns a value >=0, then that value, call it index,
* is such that n = C( sel^{C,1}( t ), ..., sel^{C,m}( t ) ),
* where C is the index^{th} constructor of dt.
*/
-int isInstCons(Node t, Node n, const Datatype& dt);
+int isInstCons(Node t, Node n, const DType& dt);
/** is tester
*
* This method returns a value >=0 if n is a tester predicate. The return
* index of a selector in its constructor. (Zero is always the
* first index.)
*/
-unsigned indexOf(Node n);
+size_t indexOf(Node n);
+/**
+ * Get the index of constructor corresponding to selector.
+ * (Zero is always the first index.)
+ */
+size_t cindexOf(Node n);
+/**
+ * Get the datatype of n.
+ */
+const DType& datatypeOf(Node n);
/** make tester is-C( n ), where C is the i^{th} constructor of dt */
-Node mkTester(Node n, int i, const Datatype& dt);
+Node mkTester(Node n, int i, const DType& dt);
/** make tester split
*
* Returns the formula (OR is-C1( n ) ... is-Ck( n ) ), where C1...Ck
* are the constructors of n's type (dt).
*/
-Node mkSplit(Node n, const Datatype& dt);
+Node mkSplit(Node n, const DType& dt);
/** returns true iff n is a constructor term with no datatype children */
bool isNullaryApplyConstructor(Node n);
/** returns true iff c is a constructor with no datatype children */
-bool isNullaryConstructor(const DatatypeConstructor& c);
+bool isNullaryConstructor(const DTypeConstructor& c);
/** check clash
*
* This method returns true if and only if n1 and n2 have a skeleton that has
* encodes. If doBetaReduction is true, then lambdas are eagerly eliminated
* via beta reduction.
*/
-Node mkSygusTerm(const Datatype& dt,
+Node mkSygusTerm(const DType& dt,
unsigned i,
const std::vector<Node>& children,
bool doBetaReduction = true);
* to cache the results of whether the evaluation of this constructor needs
* a substitution over the formal argument list of the function-to-synthesize.
*/
-Node applySygusArgs(const Datatype& dt,
+Node applySygusArgs(const DType& dt,
Node op,
Node n,
const std::vector<Node>& args);
{
Debug("dt-enum-debug")
<< "Look at constructor " << (index - d_has_debruijn) << std::endl;
- DatatypeConstructor ctor = d_datatype[index - d_has_debruijn];
+ const DTypeConstructor& ctor = d_datatype[index - d_has_debruijn];
Debug("dt-enum-debug") << "Check last term..." << std::endl;
// we first check if the last argument (which is forced to make sum of
// iterated arguments equal to d_size_limit) is defined
}
Debug("dt-enum-debug") << "Get constructor..." << std::endl;
NodeBuilder<> b(kind::APPLY_CONSTRUCTOR);
- Type typ;
if (d_datatype.isParametric())
{
- typ = ctor.getSpecializedConstructorType(d_type.toType());
- b << NodeManager::currentNM()->mkNode(
- kind::APPLY_TYPE_ASCRIPTION,
- NodeManager::currentNM()->mkConst(AscriptionType(typ)),
- Node::fromExpr(ctor.getConstructor()));
+ NodeManager* nm = NodeManager::currentNM();
+ TypeNode typ = ctor.getSpecializedConstructorType(d_type);
+ b << nm->mkNode(kind::APPLY_TYPE_ASCRIPTION,
+ nm->mkConst(AscriptionType(typ.toType())),
+ ctor.getConstructor());
}
else
{
Debug("dt-enum") << "datatype is kind " << d_type.getKind() << std::endl;
Debug("dt-enum") << "datatype is " << d_type << std::endl;
Debug("dt-enum") << "properties : " << d_datatype.isCodatatype() << " "
- << d_datatype.isRecursiveSingleton(d_type.toType());
- Debug("dt-enum") << " " << d_datatype.isInterpretedFinite(d_type.toType())
+ << d_datatype.isRecursiveSingleton(d_type);
+ Debug("dt-enum") << " " << d_datatype.isInterpretedFinite(d_type)
<< std::endl;
if (d_datatype.isCodatatype() && hasCyclesDt(d_datatype))
// this datatype. Since datatypes can not be embedded in non-datatype
// types (e.g. (Array D D) cannot be a subfield type of datatype D), this
// call is guaranteed to avoid infinite recursion.
- d_zeroTerm = Node::fromExpr(d_datatype.mkGroundValue(d_type.toType()));
+ d_zeroTerm = d_datatype.mkGroundValue(d_type);
d_zeroTermActive = true;
Debug("dt-enum-debug") << "done : " << d_zeroTerm << std::endl;
Assert(d_zeroTerm.getKind() == kind::APPLY_CONSTRUCTOR);
d_sel_types.push_back(std::vector<TypeNode>());
d_sel_index.push_back(std::vector<unsigned>());
d_sel_sum.push_back(-1);
- DatatypeConstructor ctor = d_datatype[i];
- Type typ;
+ const DTypeConstructor& ctor = d_datatype[i];
+ TypeNode typ;
if (d_datatype.isParametric())
{
- typ = ctor.getSpecializedConstructorType(d_type.toType());
+ typ = ctor.getSpecializedConstructorType(d_type);
}
for (unsigned a = 0; a < ctor.getNumArgs(); ++a)
{
TypeNode tn;
if (d_datatype.isParametric())
{
- tn = TypeNode::fromType(typ)[a];
+ tn = typ[a];
}
else
{
- tn = Node::fromExpr(ctor[a].getSelector()).getType()[1];
+ tn = ctor[a].getSelector().getType()[1];
}
d_sel_types.back().push_back(tn);
d_sel_index.back().push_back(0);
// or other cases
if (prevSize == d_size_limit
|| (d_size_limit == 0 && d_datatype.isCodatatype())
- || !d_datatype.isInterpretedFinite(d_type.toType()))
+ || !d_datatype.isInterpretedFinite(d_type))
{
d_size_limit++;
d_ctor = 0;
#ifndef CVC4__THEORY__DATATYPES__TYPE_ENUMERATOR_H
#define CVC4__THEORY__DATATYPES__TYPE_ENUMERATOR_H
-#include "theory/type_enumerator.h"
-#include "expr/type_node.h"
-#include "expr/type.h"
+#include "expr/dtype.h"
#include "expr/kind.h"
+#include "expr/type.h"
+#include "expr/type_node.h"
#include "options/quantifiers_options.h"
+#include "theory/type_enumerator.h"
namespace CVC4 {
namespace theory {
/** type properties */
TypeEnumeratorProperties * d_tep;
/** The datatype we're enumerating */
- const Datatype& d_datatype;
+ const DType& d_datatype;
/** extra cons */
unsigned d_has_debruijn;
/** type */
/** child */
bool d_child_enum;
- bool hasCyclesDt( const Datatype& dt ) {
- return dt.isRecursiveSingleton( d_type.toType() ) || !dt.isFinite( d_type.toType() );
+ bool hasCyclesDt(const DType& dt)
+ {
+ return dt.isRecursiveSingleton(d_type) || !dt.isFinite(d_type);
}
bool hasCycles( TypeNode tn ){
if( tn.isDatatype() ){
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ const DType& dt = tn.getDType();
return hasCyclesDt( dt );
}else{
return false;
DatatypesEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr)
: TypeEnumeratorBase<DatatypesEnumerator>(type),
d_tep(tep),
- d_datatype(DatatypeType(type.toType()).getDatatype()),
+ d_datatype(type.getDType()),
d_type(type),
d_ctor(0),
d_zeroTermActive(false)
TypeEnumeratorProperties* tep = nullptr)
: TypeEnumeratorBase<DatatypesEnumerator>(type),
d_tep(tep),
- d_datatype(DatatypeType(type.toType()).getDatatype()),
+ d_datatype(type.getDType()),
d_type(type),
d_ctor(0),
d_zeroTermActive(false)
#include "theory/quantifiers/cegqi/ceg_dt_instantiator.h"
+#include "expr/dtype.h"
#include "expr/node_algorithm.h"
+#include "theory/datatypes/theory_datatypes_utils.h"
using namespace std;
using namespace CVC4::kind;
<< "...try based on constructor term " << n << std::endl;
std::vector<Node> children;
children.push_back(n.getOperator());
- const Datatype& dt =
- static_cast<DatatypeType>(d_type.toType()).getDatatype();
- unsigned cindex = Datatype::indexOf(n.getOperator().toExpr());
+ const DType& dt = d_type.getDType();
+ unsigned cindex = datatypes::utils::indexOf(n.getOperator());
// now must solve for selectors applied to pv
for (unsigned j = 0, nargs = dt[cindex].getNumArgs(); j < nargs; j++)
{
- Node c = nm->mkNode(
- APPLY_SELECTOR_TOTAL,
- Node::fromExpr(dt[cindex].getSelectorInternal(d_type.toType(), j)),
- pv);
+ Node c = nm->mkNode(APPLY_SELECTOR_TOTAL,
+ dt[cindex].getSelectorInternal(d_type, j),
+ pv);
ci->pushStackVariable(c);
children.push_back(c);
}
else
{
NodeManager* nm = NodeManager::currentNM();
- unsigned cindex = Datatype::indexOf(a.getOperator().toExpr());
+ unsigned cindex = DType::indexOf(a.getOperator().toExpr());
TypeNode tn = a.getType();
- const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+ const DType& dt = tn.getDType();
for (unsigned i = 0, nchild = a.getNumChildren(); i < nchild; i++)
{
Node nn = nm->mkNode(
- APPLY_SELECTOR_TOTAL,
- Node::fromExpr(dt[cindex].getSelectorInternal(tn.toType(), i)),
- sb);
+ APPLY_SELECTOR_TOTAL, dt[cindex].getSelectorInternal(tn, i), sb);
Node s = solve_dt(v, a[i], Node::null(), sa[i], nn);
if (!s.isNull())
{
// we initialize to handled, we remain handled as long as all subfields
// of this datatype are not unhandled.
ret = CEG_HANDLED;
- const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+ const DType& dt = tn.getDType();
for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
{
for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
{
- TypeNode crange = TypeNode::fromType(
- static_cast<SelectorType>(dt[i][j].getType()).getRangeType());
+ TypeNode crange = dt[i].getArgType(j);
CegHandledStatus cret = isCbqiSort(crange, visited, qe);
if (cret == CEG_UNHANDLED)
{
registerTheoryId(tid);
if (tn.isDatatype())
{
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ const DType& dt = tn.getDType();
for (unsigned i = 0; i < dt.getNumConstructors(); i++)
{
for (unsigned j = 0; j < dt[i].getNumArgs(); j++)
{
- registerTheoryIds(
- TypeNode::fromType(
- ((SelectorType)dt[i][j].getType()).getRangeType()),
- visited);
+ registerTheoryIds(dt[i].getArgType(j), visited);
}
}
}
**/
#include "theory/quantifiers/ematching/candidate_generator.h"
+#include "expr/dtype.h"
#include "options/quantifiers_options.h"
#include "theory/quantifiers/inst_match.h"
#include "theory/quantifiers/instantiate.h"
: CandidateGeneratorQE(qe, mpat)
{
Assert(mpat.getKind() == APPLY_CONSTRUCTOR);
- d_mpat_type = static_cast<DatatypeType>(mpat.getType().toType());
+ d_mpat_type = mpat.getType();
}
void CandidateGeneratorConsExpand::reset(Node eqc)
{
d_eqc = eqc;
d_mode = cand_term_ident;
- Assert(d_eqc.getType().toType() == d_mpat_type);
+ Assert(d_eqc.getType() == d_mpat_type);
}
}
// expand it
NodeManager* nm = NodeManager::currentNM();
std::vector<Node> children;
- const Datatype& dt = d_mpat_type.getDatatype();
+ const DType& dt = d_mpat_type.getDType();
Assert(dt.getNumConstructors() == 1);
children.push_back(d_op);
for (unsigned i = 0, nargs = dt[0].getNumArgs(); i < nargs; i++)
{
- Node sel =
- nm->mkNode(APPLY_SELECTOR_TOTAL,
- Node::fromExpr(dt[0].getSelectorInternal(d_mpat_type, i)),
- curr);
+ Node sel = nm->mkNode(
+ APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal(d_mpat_type, i), curr);
children.push_back(sel);
}
return nm->mkNode(APPLY_CONSTRUCTOR, children);
protected:
/** the (datatype) type of the input match pattern */
- DatatypeType d_mpat_type;
+ TypeNode d_mpat_type;
/** we don't care about the operator of n */
bool isLegalOpCandidate(Node n) override;
};
#include "expr/datatype.h"
#include "options/datatypes_options.h"
#include "options/quantifiers_options.h"
+#include "theory/datatypes/theory_datatypes_utils.h"
#include "theory/quantifiers/ematching/candidate_generator.h"
#include "theory/quantifiers/ematching/trigger.h"
#include "theory/quantifiers/instantiate.h"
{
// 1-constructors have a trivial way of generating candidates in a
// given equivalence class
- const Datatype& dt = d_match_pattern.getType().getDatatype();
+ const DType& dt = d_match_pattern.getType().getDType();
if (dt.getNumConstructors() == 1)
{
d_cg = new inst::CandidateGeneratorConsExpand(qe, d_match_pattern);
}
}else if( d_match_pattern.getKind()==INST_CONSTANT ){
if( d_pattern.getKind()==APPLY_SELECTOR_TOTAL ){
- Expr selectorExpr = qe->getTermDatabase()->getMatchOperator( d_pattern ).toExpr();
- size_t selectorIndex = Datatype::cindexOf(selectorExpr);
- const Datatype& dt = Datatype::datatypeOf(selectorExpr);
- const DatatypeConstructor& c = dt[selectorIndex];
- Node cOp = Node::fromExpr(c.getConstructor());
+ Node selectorExpr = qe->getTermDatabase()->getMatchOperator(d_pattern);
+ size_t selectorIndex = datatypes::utils::cindexOf(selectorExpr);
+ const DType& dt = datatypes::utils::datatypeOf(selectorExpr);
+ const DTypeConstructor& c = dt[selectorIndex];
+ Node cOp = c.getConstructor();
Trace("inst-match-gen") << "Purify dt trigger " << d_pattern << ", will match terms of op " << cOp << std::endl;
d_cg = new inst::CandidateGeneratorQE( qe, cOp );
}else{
#include "expr/node_algorithm.h"
#include "options/quantifiers_options.h"
#include "theory/arith/arith_msum.h"
+#include "theory/datatypes/theory_datatypes_utils.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/fmf/model_engine.h"
#include "theory/quantifiers/term_enumeration.h"
return Node::null();
}
}
- const Datatype& dt = Datatype::datatypeOf( t.getOperator().toExpr() );
- unsigned index = Datatype::indexOf( t.getOperator().toExpr() );
+ NodeManager* nm = NodeManager::currentNM();
+ const DType& dt = datatypes::utils::datatypeOf(t.getOperator());
+ unsigned index = datatypes::utils::indexOf(t.getOperator());
for( unsigned i=0; i<t.getNumChildren(); i++ ){
Node u;
if( e.getKind()==kind::APPLY_CONSTRUCTOR ){
u = matchBoundVar( v, t[i], e[i] );
}else{
- Node se = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[index].getSelectorInternal( e.getType().toType(), i ) ), e );
+ Node se = nm->mkNode(APPLY_SELECTOR_TOTAL,
+ dt[index].getSelectorInternal(e.getType(), i),
+ e);
u = matchBoundVar( v, t[i], se );
}
if( !u.isNull() ){
for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
TypeNode tn = q[0][i].getType();
if( tn.isDatatype() ){
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
- if( dt.isRecursiveSingleton( tn.toType() ) ){
+ const DType& dt = tn.getDType();
+ if (dt.isRecursiveSingleton(tn))
+ {
Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is recursive singleton." << std::endl;
- }else{
+ }
+ else
+ {
if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_AGG ){
// split if it is a finite datatype
- doSplit = dt.isInterpretedFinite(tn.toType());
+ doSplit = dt.isInterpretedFinite(tn);
}else if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_DEFAULT ){
if( !d_quantEngine->isFiniteBound( q, q[0][i] ) ){
- if (dt.isInterpretedFinite(tn.toType()))
+ if (dt.isInterpretedFinite(tn))
{
// split if goes from being unhandled -> handled by finite
// instantiation. An example is datatypes with uninterpreted sort
TypeNode tn = svar.getType();
Assert(tn.isDatatype());
std::vector<Node> cons;
- const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+ const DType& dt = tn.getDType();
for (unsigned j = 0, ncons = dt.getNumConstructors(); j < ncons; j++)
{
std::vector<Node> vars;
for (unsigned k = 0, nargs = dt[j].getNumArgs(); k < nargs; k++)
{
- TypeNode tns = TypeNode::fromType(dt[j][k].getRangeType());
+ TypeNode tns = dt[j][k].getRangeType();
Node v = nm->mkBoundVar(tns);
vars.push_back(v);
}
std::vector<Node> bvs_cmb;
bvs_cmb.insert(bvs_cmb.end(), bvs.begin(), bvs.end());
bvs_cmb.insert(bvs_cmb.end(), vars.begin(), vars.end());
- vars.insert(vars.begin(), Node::fromExpr(dt[j].getConstructor()));
+ vars.insert(vars.begin(), dt[j].getConstructor());
Node c = nm->mkNode(kind::APPLY_CONSTRUCTOR, vars);
TNode ct = c;
Node body = q[1].substitute(svar, ct);
#include "theory/quantifiers/quantifiers_rewriter.h"
+#include "expr/dtype.h"
#include "expr/node_algorithm.h"
#include "options/quantifiers_options.h"
#include "theory/arith/arith_msum.h"
+#include "theory/datatypes/theory_datatypes_utils.h"
#include "theory/quantifiers/bv_inverter.h"
#include "theory/quantifiers/ematching/trigger.h"
#include "theory/quantifiers/quantifiers_attributes.h"
Trace("quantifiers-rewrite-ite-debug") << "...condition already set " << itp->second << std::endl;
computeDtTesterIteSplit( n[ itp->second==n[0] ? 1 : 2 ], pcons, ncons, conj );
}else{
- Expr testerExpr = n[0].getOperator().toExpr();
- int index = Datatype::indexOf( testerExpr );
+ Node tester = n[0].getOperator();
+ int index = datatypes::utils::indexOf(tester);
std::map< int, Node >::iterator itn = ncons[x].find( index );
if( itn!=ncons[x].end() ){
Trace("quantifiers-rewrite-ite-debug") << "...condition negated " << itn->second << std::endl;
}
}
}else{
+ NodeManager* nm = NodeManager::currentNM();
Trace("quantifiers-rewrite-ite-debug") << "Return value : " << n << std::endl;
std::vector< Node > children;
children.push_back( n );
//only if we haven't settled on a positive tester
if( std::find( vars.begin(), vars.end(), x )==vars.end() ){
//check if we have exhausted all options but one
- const Datatype& dt = DatatypeType(x.getType().toType()).getDatatype();
+ const DType& dt = x.getType().getDType();
std::vector< Node > nchildren;
int pos_cons = -1;
for( int i=0; i<(int)dt.getNumConstructors(); i++ ){
}
}
if( pos_cons>=0 ){
- const DatatypeConstructor& c = dt[pos_cons];
- Expr tester = c.getTester();
- children.push_back( NodeManager::currentNM()->mkNode( kind::APPLY_TESTER, Node::fromExpr( tester ), x ).negate() );
+ Node tester = dt[pos_cons].getTester();
+ children.push_back(nm->mkNode(APPLY_TESTER, tester, x).negate());
}else{
children.insert( children.end(), nchildren.begin(), nchildren.end() );
}
}
if( addEntailedCond( n, pol, currCond, new_cond, conflict ) ){
if( n.getKind()==APPLY_TESTER ){
- const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr());
- unsigned index = Datatype::indexOf(n.getOperator().toExpr());
+ NodeManager* nm = NodeManager::currentNM();
+ const DType& dt = datatypes::utils::datatypeOf(n.getOperator());
+ unsigned index = datatypes::utils::indexOf(n.getOperator());
Assert(dt.getNumConstructors() > 1);
if( pol ){
for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
if( i!=index ){
- Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), n[0] );
+ Node t = nm->mkNode(APPLY_TESTER, dt[i].getTester(), n[0]);
addEntailedCond( t, false, currCond, new_cond, conflict );
}
}
}else{
if( dt.getNumConstructors()==2 ){
int oindex = 1-index;
- Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[oindex].getTester() ), n[0] );
+ Node t = nm->mkNode(APPLY_TESTER, dt[oindex].getTester(), n[0]);
addEntailedCond( t, true, currCond, new_cond, conflict );
}
}
if (ita != args.end())
{
vars.push_back(lit[0]);
- Expr testerExpr = lit.getOperator().toExpr();
- int index = Datatype::indexOf(testerExpr);
- const Datatype& dt = Datatype::datatypeOf(testerExpr);
- const DatatypeConstructor& c = dt[index];
+ Node tester = lit.getOperator();
+ int index = datatypes::utils::indexOf(tester);
+ const DType& dt = datatypes::utils::datatypeOf(tester);
+ const DTypeConstructor& c = dt[index];
std::vector<Node> newChildren;
- newChildren.push_back(Node::fromExpr(c.getConstructor()));
+ newChildren.push_back(c.getConstructor());
std::vector<Node> newVars;
for (unsigned j = 0, nargs = c.getNumArgs(); j < nargs; j++)
{
- TypeNode tn = TypeNode::fromType(c[j].getRangeType());
+ TypeNode tn = c[j].getRangeType();
Node v = nm->mkBoundVar(tn);
newChildren.push_back(v);
newVars.push_back(v);
{
Trace("var-elim-dt") << "Expand datatype variable based on : " << lit
<< std::endl;
- Expr testerExpr = lit.getOperator().toExpr();
- unsigned index = Datatype::indexOf(testerExpr);
+ Node tester = lit.getOperator();
+ unsigned index = datatypes::utils::indexOf(tester);
Node s = datatypeExpand(index, lit[0], args);
if (!s.isNull())
{
{
return Node::null();
}
- const Datatype& dt =
- static_cast<DatatypeType>(v.getType().toType()).getDatatype();
+ const DType& dt = v.getType().getDType();
Assert(index < dt.getNumConstructors());
- const DatatypeConstructor& c = dt[index];
+ const DTypeConstructor& c = dt[index];
std::vector<Node> newChildren;
- newChildren.push_back(Node::fromExpr(c.getConstructor()));
+ newChildren.push_back(c.getConstructor());
std::vector<Node> newVars;
for (unsigned j = 0, nargs = c.getNumArgs(); j < nargs; j++)
{
- TypeNode tn = TypeNode::fromType(c.getArgType(j));
+ TypeNode tn = c.getArgType(j);
Node vn = NodeManager::currentNM()->mkBoundVar(tn);
newChildren.push_back(vn);
newVars.push_back(vn);
return Node::null();
}
-void Skolemize::getSelfSel(const Datatype& dt,
- const DatatypeConstructor& dc,
+void Skolemize::getSelfSel(const DType& dt,
+ const DTypeConstructor& dc,
Node n,
TypeNode ntn,
std::vector<Node>& selfSel)
TypeNode tspec;
if (dt.isParametric())
{
- tspec = TypeNode::fromType(
- dc.getSpecializedConstructorType(n.getType().toType()));
+ tspec = dc.getSpecializedConstructorType(n.getType());
Trace("sk-ind-debug") << "Specialized constructor type : " << tspec
<< std::endl;
Assert(tspec.getNumChildren() == dc.getNumArgs());
}
Trace("sk-ind-debug") << "Check self sel " << dc.getName() << " "
<< dt.getName() << std::endl;
+ NodeManager* nm = NodeManager::currentNM();
for (unsigned j = 0; j < dc.getNumArgs(); j++)
{
std::vector<Node> ssc;
}
else
{
- TypeNode tn = TypeNode::fromType(dc[j].getRangeType());
+ TypeNode tn = dc[j].getRangeType();
Trace("sk-ind-debug") << "Compare " << tn << " " << ntn << std::endl;
if (tn == ntn)
{
ssc.push_back(n);
}
}
- /* TODO: more than weak structural induction
- else if( tn.isDatatype() && std::find( visited.begin(), visited.end(), tn
- )==visited.end() ){
- visited.push_back( tn );
- const Datatype& dt =
- ((DatatypeType)(subs[0].getType()).toType()).getDatatype();
- std::vector< Node > disj;
- for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
- getSelfSel( dt[i], n, ntn, ssc );
- }
- visited.pop_back();
- }
- */
for (unsigned k = 0; k < ssc.size(); k++)
{
- Node ss = NodeManager::currentNM()->mkNode(
- APPLY_SELECTOR_TOTAL,
- dc.getSelectorInternal(n.getType().toType(), j),
- n);
+ Node ss = nm->mkNode(
+ APPLY_SELECTOR_TOTAL, dc.getSelectorInternal(n.getType(), j), n);
if (std::find(selfSel.begin(), selfSel.end(), ss) == selfSel.end())
{
selfSel.push_back(ss);
Node& sub,
std::vector<unsigned>& sub_vars)
{
+ NodeManager* nm = NodeManager::currentNM();
Assert(sk.empty() || sk.size() == f[0].getNumChildren());
// calculate the variables and substitution
std::vector<TNode> ind_vars;
// the following constructs ~( R( x, k ) => ~P( x ) )
if (options::dtStcInduction() && tn.isDatatype())
{
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ const DType& dt = tn.getDType();
std::vector<Node> disj;
for (unsigned i = 0; i < dt.getNumConstructors(); i++)
{
std::vector<Node> selfSel;
getSelfSel(dt, dt[i], k, tn, selfSel);
std::vector<Node> conj;
- conj.push_back(
- NodeManager::currentNM()
- ->mkNode(APPLY_TESTER, Node::fromExpr(dt[i].getTester()), k)
- .negate());
+ conj.push_back(nm->mkNode(APPLY_TESTER, dt[i].getTester(), k).negate());
for (unsigned j = 0; j < selfSel.size(); j++)
{
conj.push_back(ret.substitute(ind_vars[0], selfSel[j]).negate());
TypeNode tn = n.getType();
if (options::dtStcInduction() && tn.isDatatype())
{
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ const DType& dt = tn.getDType();
return !dt.isCodatatype();
}
if (options::intWfInduction() && n.getType().isInteger())
* applied to term n, whose return type in ntn, and stores
* them in the vector selfSel.
*/
- static void getSelfSel(const Datatype& dt,
- const DatatypeConstructor& dc,
+ static void getSelfSel(const DType& dt,
+ const DTypeConstructor& dc,
Node n,
TypeNode ntn,
std::vector<Node>& selfSel);
bool rconsSygus)
{
Assert(d_sol != NULL);
- const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
- Node varList = Node::fromExpr( dt.getSygusVarList() );
+ const DType& dt = stn.getDType();
+ Node varList = dt.getSygusVarList();
Node prog = d_quant[0][sol_index];
std::vector< Node > vars;
Node s;
|| d_inst.empty())
{
Trace("csi-sol") << "Get solution for (unconstrained) " << prog << std::endl;
- s = d_qe->getTermEnumeration()->getEnumerateTerm(
- TypeNode::fromType(dt.getSygusType()), 0);
+ s = d_qe->getTermEnumeration()->getEnumerateTerm(dt.getSygusType(), 0);
}
else
{
bool rconsSygus)
{
d_solution = s;
- const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
+ const DType& dt = stn.getDType();
//reconstruct the solution into sygus if necessary
reconstructed = 0;
}
//make into lambda
if( !dt.getSygusVarList().isNull() ){
- Node varList = Node::fromExpr( dt.getSygusVarList() );
+ Node varList = dt.getSygusVarList();
return NodeManager::currentNM()->mkNode( LAMBDA, varList, sol );
}else{
return sol;
#include "theory/quantifiers/sygus/ce_guided_single_inv_sol.h"
#include "expr/datatype.h"
+#include "expr/dtype.h"
#include "expr/node_algorithm.h"
#include "options/quantifiers_options.h"
#include "theory/arith/arith_msum.h"
#include "theory/quantifiers/term_enumeration.h"
#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
-#include "theory/theory_engine.h"
using namespace CVC4::kind;
using namespace std;
{
TypeNode tn = it->first;
Assert(tn.isDatatype());
- const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+ const DType& dt = tn.getDType();
Trace("csi-rcons") << "Terms to reconstruct of type " << dt.getName()
<< " : " << std::endl;
for (std::map<Node, int>::iterator it2 = it->second.begin();
d_rcons_to_status[stn][t] = -1;
TypeNode tn = t.getType();
Assert(stn.isDatatype());
- const Datatype& dt = stn.getDatatype();
+ const DType& dt = stn.getDType();
TermDbSygus* tds = d_qe->getTermDatabaseSygus();
SygusTypeInfo& sti = tds->getTypeInfo(stn);
Assert(dt.isSygus());
carg = sti.getOpConsNum(min_t);
if( carg!=-1 ){
Trace("csi-rcons-debug") << " Type has operator." << std::endl;
- d_reconstruct[id] = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, Node::fromExpr( dt[carg].getConstructor() ) );
+ d_reconstruct[id] = NodeManager::currentNM()->mkNode(
+ APPLY_CONSTRUCTOR, dt[carg].getConstructor());
status = 0;
}else{
//check if kind is in syntax sort
if( tchildren.size()==dt[karg].getNumArgs() ){
Trace("csi-rcons-debug") << "Type for " << id << " has kind " << min_t.getKind() << ", recurse." << std::endl;
status = 0;
- Node cons = Node::fromExpr( dt[karg].getConstructor() );
+ Node cons = dt[karg].getConstructor();
if( !collectReconstructNodes( id, tchildren, dt[karg], d_reconstruct_op[id][cons], status ) ){
Trace("csi-rcons-debug") << "...failure for " << id << " " << dt[karg].getName() << std::endl;
d_reconstruct_op[id].erase( cons );
//try to directly reconstruct from single argument
std::vector< Node > tchildren;
tchildren.push_back( min_t );
- TypeNode stnc = TypeNode::fromType( ((SelectorType)dt[ii][0].getType()).getRangeType() );
+ TypeNode stnc = dt[ii][0].getRangeType();
Trace("csi-rcons-debug") << "...try identity function " << dt[ii].getSygusOp() << ", child type is " << stnc << std::endl;
status = 0;
- Node cons = Node::fromExpr( dt[ii].getConstructor() );
+ Node cons = dt[ii].getConstructor();
if( !collectReconstructNodes( id, tchildren, dt[ii], d_reconstruct_op[id][cons], status ) ){
d_reconstruct_op[id].erase( cons );
status = 1;
{
success = true;
status = 0;
- Node cons = Node::fromExpr( dt[index_found].getConstructor() );
+ Node cons = dt[index_found].getConstructor();
Trace("csi-rcons-debug") << "Try alternative for " << id << ", matching " << dt[index_found].getName() << " with children : " << std::endl;
for( unsigned i=0; i<args.size(); i++ ){
Trace("csi-rcons-debug") << " " << args[i] << std::endl;
bool CegSingleInvSol::collectReconstructNodes(int pid,
std::vector<Node>& ts,
- const DatatypeConstructor& dtc,
+ const DTypeConstructor& dtc,
std::vector<int>& ids,
int& status)
{
if( it==d_rcons_to_id[stn].end() ){
int ret = d_id_count;
if( Trace.isOn("csi-rcons-debug") ){
- const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
+ const DType& dt = stn.getDType();
Trace("csi-rcons-debug") << "id " << ret << " : " << n << " " << dt.getName() << std::endl;
}
d_id_node[d_id_count] = n;
d_builtin_const_to_sygus[tn][c] = c;
return c;
}
- const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+ const DType& dt = tn.getDType();
Trace("csi-rcons-debug") << "Try to reconstruct " << c << " in "
<< dt.getName() << std::endl;
if (!dt.isSygus())
int carg = ti.getOpConsNum(c);
if (carg != -1)
{
- sc = nm->mkNode(APPLY_CONSTRUCTOR,
- Node::fromExpr(dt[carg].getConstructor()));
+ sc = nm->mkNode(APPLY_CONSTRUCTOR, dt[carg].getConstructor());
}
else
{
Node n = builtinToSygusConst(c, tnc, rcons_depth);
if (!n.isNull())
{
- sc = nm->mkNode(
- APPLY_CONSTRUCTOR, Node::fromExpr(dt[ii].getConstructor()), n);
+ sc = nm->mkNode(APPLY_CONSTRUCTOR, dt[ii].getConstructor(), n);
break;
}
}
if (rcons_depth < 1000)
{
// accelerated, recursive reconstruction of constants
- Kind pk = getPlusKind(TypeNode::fromType(dt.getSygusType()));
+ Kind pk = getPlusKind(dt.getSygusType());
if (pk != UNDEFINED_KIND)
{
int arg = ti.getKindConsNum(pk);
if (arg != -1)
{
- Kind ck =
- getComparisonKind(TypeNode::fromType(dt.getSygusType()));
- Kind pkm =
- getPlusKind(TypeNode::fromType(dt.getSygusType()), true);
+ Kind ck = getComparisonKind(dt.getSygusType());
+ Kind pkm = getPlusKind(dt.getSygusType(), true);
// get types
Assert(dt[arg].getNumArgs() == 2);
TypeNode tn1 = tds->getArgType(dt[arg], 0);
Node sc1 = builtinToSygusConst(c1, tn1, rcons_depth);
Assert(!sc1.isNull());
sc = nm->mkNode(APPLY_CONSTRUCTOR,
- Node::fromExpr(dt[arg].getConstructor()),
+ dt[arg].getConstructor(),
sc1,
sc2);
break;
TermDbSygus* tds = d_qe->getTermDatabaseSygus();
// ensure it is registered
tds->registerSygusType(tn);
- const Datatype& dt = tn.getDatatype();
+ const DType& dt = tn.getDType();
Assert(dt.isSygus());
- TypeNode btn = TypeNode::fromType(dt.getSygusType());
+ TypeNode btn = dt.getSygusType();
// for constant reconstruction
Kind ck = getComparisonKind(btn);
Node z = d_qe->getTermUtil()->getTypeValue(btn, 0);
// iterate over constructors
for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
{
- Node n = Node::fromExpr(dt[i].getSygusOp());
+ Node n = dt[i].getSygusOp();
if (n.getKind() != kind::BUILTIN && n.isConst())
{
d_const_list[tn].push_back(n);
int index_start)
{
Assert(st.isDatatype());
- const Datatype& dt = static_cast<DatatypeType>(st.toType()).getDatatype();
+ const DType& dt = st.getDType();
Assert(dt.isSygus());
std::map<Kind, std::vector<Node> > kgens;
std::vector<Node> gens;
return false;
}
-Node CegSingleInvSol::getGenericBase(TypeNode tn, const Datatype& dt, int c)
+Node CegSingleInvSol::getGenericBase(TypeNode tn, const DType& dt, int c)
{
std::map<int, Node>::iterator it = d_generic_base[tn].find(c);
if (it != d_generic_base[tn].end())
int allocate( Node n, TypeNode stn );
// term t with sygus type st, returns inducted templated form of t
int collectReconstructNodes( Node t, TypeNode stn, int& status );
- bool collectReconstructNodes( int pid, std::vector< Node >& ts, const DatatypeConstructor& dtc, std::vector< int >& ids, int& status );
+ bool collectReconstructNodes(int pid,
+ std::vector<Node>& ts,
+ const DTypeConstructor& dtc,
+ std::vector<int>& ids,
+ int& status);
bool getPathToRoot( int id );
void setReconstructed( int id, Node n );
//get equivalent terms to n with top symbol k
* This returns the builtin term that is the analog of an application of the
* c^th constructor of dt to fresh variables.
*/
- Node getGenericBase(TypeNode tn, const Datatype& dt, int c);
+ Node getGenericBase(TypeNode tn, const DType& dt, int c);
/** cache for the above function */
std::map<TypeNode, std::map<int, Node> > d_generic_base;
/** get match
// candidate has the production rule gt -> AND( gt, gt ). Similarly for
// precondition and OR.
Assert(gt.isDatatype());
- const Datatype& gdt = gt.getDatatype();
+ const DType& gdt = gt.getDType();
SygusTypeInfo& gti = d_tds->getTypeInfo(gt);
for (unsigned r = 0; r < 2; r++)
{
Kind rk = r == 0 ? OR : AND;
int i = gti.getKindConsNum(rk);
if (i != -1 && gdt[i].getNumArgs() == 2
- && TypeNode::fromType(gdt[i].getArgType(0)) == gt
- && TypeNode::fromType(gdt[i].getArgType(1)) == gt)
+ && gdt[i].getArgType(0) == gt
+ && gdt[i].getArgType(1) == gt)
{
Trace("sygus-ccore-init") << " will do " << (r == 0 ? "pre" : "post")
<< "condition." << std::endl;
- Node cons = Node::fromExpr(gdt[i].getConstructor());
+ Node cons = gdt[i].getConstructor();
c.initialize(f, cons);
// Register the symmetry breaking lemma: do not do top-level solutions
// with this constructor (e.g. we want to enumerate literals, not
d_value = value;
// get variables in value's type
TypeNode tn = value.getType();
- Node var_list = Node::fromExpr(tn.getDatatype().getSygusVarList());
+ Node var_list = tn.getDType().getSygusVarList();
NodeManager* nm = NodeManager::currentNM();
// get subtypes in value's type
SygusTypeInfo& ti = d_tds->getTypeInfo(tn);
// collect constructors for variable in all subtypes
for (const TypeNode& stn : sf_types)
{
- const Datatype& dt = stn.getDatatype();
+ const DType& dt = stn.getDType();
for (unsigned i = 0, size = dt.getNumConstructors(); i < size; ++i)
{
- if (dt[i].getNumArgs() == 0 && Node::fromExpr(dt[i].getSygusOp()) == v)
+ if (dt[i].getNumArgs() == 0 && dt[i].getSygusOp() == v)
{
Node cons = nm->mkNode(APPLY_CONSTRUCTOR, dt[i].getConstructor());
d_var_tn_cons[v][stn] = cons;
{
d_tn = tn;
// get variables in value's type
- Node var_list = Node::fromExpr(tn.getDatatype().getSygusVarList());
+ Node var_list = tn.getDType().getSygusVarList();
// get subtypes in value's type
NodeManager* nm = NodeManager::currentNM();
SygusTypeInfo& ti = d_tds->getTypeInfo(tn);
// collect constructors for variable in all subtypes
for (const TypeNode& stn : sf_types)
{
- const Datatype& dt = stn.getDatatype();
+ const DType& dt = stn.getDType();
for (unsigned i = 0, size = dt.getNumConstructors(); i < size; ++i)
{
- if (dt[i].getNumArgs() == 0 && Node::fromExpr(dt[i].getSygusOp()) == v)
+ if (dt[i].getNumArgs() == 0 && dt[i].getSygusOp() == v)
{
d_var_tn_cons[v][stn] =
nm->mkNode(APPLY_CONSTRUCTOR, dt[i].getConstructor());
#include "theory/quantifiers/sygus/sygus_abduct.h"
#include "expr/datatype.h"
+#include "expr/dtype.h"
#include "expr/node_algorithm.h"
#include "expr/sygus_datatype.h"
#include "printer/sygus_print_callback.h"
+#include "theory/datatypes/theory_datatypes_utils.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/quantifiers_rewriter.h"
#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
// if provided, we will associate it with the function-to-synthesize
if (!abdGType.isNull())
{
- Assert(abdGType.isDatatype() && abdGType.getDatatype().isSygus());
+ Assert(abdGType.isDatatype() && abdGType.getDType().isSygus());
// must convert all constructors to version with bound variables in "vars"
std::vector<SygusDatatype> sdts;
std::set<Type> unres;
Trace("sygus-abduct-debug") << "Process abduction type:" << std::endl;
- Trace("sygus-abduct-debug") << abdGType.getDatatype() << std::endl;
+ Trace("sygus-abduct-debug") << abdGType.getDType().getName() << std::endl;
// datatype types we need to process
std::vector<TypeNode> dtToProcess;
std::map<TypeNode, TypeNode> dtProcessed;
dtToProcess.push_back(abdGType);
std::stringstream ssutn0;
- ssutn0 << abdGType.getDatatype().getName() << "_s";
+ ssutn0 << abdGType.getDType().getName() << "_s";
TypeNode abdTNew =
nm->mkSort(ssutn0.str(), ExprManager::SORT_FLAG_PLACEHOLDER);
unres.insert(abdTNew.toType());
std::vector<TypeNode> dtNextToProcess;
for (const TypeNode& curr : dtToProcess)
{
- Assert(curr.isDatatype() && curr.getDatatype().isSygus());
- const Datatype& dtc = curr.getDatatype();
+ Assert(curr.isDatatype() && curr.getDType().isSygus());
+ const DType& dtc = curr.getDType();
std::stringstream ssdtn;
ssdtn << dtc.getName() << "_s";
sdts.push_back(SygusDatatype(ssdtn.str()));
<< std::endl;
for (unsigned j = 0, ncons = dtc.getNumConstructors(); j < ncons; j++)
{
- Node op = Node::fromExpr(dtc[j].getSygusOp());
+ Node op = dtc[j].getSygusOp();
// apply the substitution to the argument
Node ops = op.substitute(
syms.begin(), syms.end(), varlist.begin(), varlist.end());
std::vector<TypeNode> cargs;
for (unsigned k = 0, nargs = dtc[j].getNumArgs(); k < nargs; k++)
{
- TypeNode argt = TypeNode::fromType(dtc[j].getArgType(k));
+ TypeNode argt = dtc[j].getArgType(k);
std::map<TypeNode, TypeNode>::iterator itdp =
dtProcessed.find(argt);
TypeNode argtNew;
if (itdp == dtProcessed.end())
{
std::stringstream ssutn;
- ssutn << argt.getDatatype().getName() << "_s";
+ ssutn << argt.getDType().getName() << "_s";
argtNew =
nm->mkSort(ssutn.str(), ExprManager::SORT_FLAG_PLACEHOLDER);
Trace("sygus-abduct-debug")
}
Trace("sygus-abduct-debug")
<< "Set sygus : " << dtc.getSygusType() << " " << abvl << std::endl;
- TypeNode stn = TypeNode::fromType(dtc.getSygusType());
+ TypeNode stn = dtc.getSygusType();
sdts.back().initializeDatatype(
stn, abvl, dtc.getSygusAllowConst(), dtc.getSygusAllowAll());
}
Trace("sygus-abduct-debug") << "Made datatype types:" << std::endl;
for (unsigned j = 0, ndts = datatypeTypes.size(); j < ndts; j++)
{
- const Datatype& dtj = datatypeTypes[j].getDatatype();
+ const DType& dtj = TypeNode::fromType(datatypeTypes[j]).getDType();
Trace("sygus-abduct-debug") << "#" << j << ": " << dtj << std::endl;
for (unsigned k = 0, ncons = dtj.getNumConstructors(); k < ncons; k++)
{
d_enum = e;
d_etype = d_enum.getType();
Assert(d_etype.isDatatype());
- Assert(d_etype.getDatatype().isSygus());
+ Assert(d_etype.getDType().isSygus());
d_tlEnum = getMasterEnumForType(d_etype);
d_abortSize = options::sygusAbortSize();
TNode agt = ag;
TNode truent = truen;
Assert(d_tcache.find(d_etype) != d_tcache.end());
- const Datatype& dt = d_etype.getDatatype();
+ const DType& dt = d_etype.getDType();
for (const Node& lem : sbl)
{
if (!d_tds->isSymBreakLemmaTemplate(lem))
{
if (a == e)
{
- Node cons = Node::fromExpr(dt[tst].getConstructor());
+ Node cons = dt[tst].getConstructor();
Trace("sygus-enum") << " ...unit exclude constructor #" << tst
<< ", constructor " << cons << std::endl;
d_sbExcTlCons.insert(cons);
// not a datatype, finish
return;
}
- const Datatype& dt = tn.getDatatype();
+ const DType& dt = tn.getDType();
if (!dt.isSygus())
{
// not a sygus datatype, finish
// record type information
for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
{
- TypeNode tn = TypeNode::fromType(dt[i].getArgType(j));
+ TypeNode tn = dt[i].getArgType(j);
argTypes[i].push_back(tn);
}
}
SygusEnumerator::TermEnum* SygusEnumerator::getMasterEnumForType(TypeNode tn)
{
- if (tn.isDatatype() && tn.getDatatype().isSygus())
+ if (tn.isDatatype() && tn.getDType().isSygus())
{
std::map<TypeNode, TermEnumMaster>::iterator it = d_masterEnum.find(tn);
if (it != d_masterEnum.end())
d_currTermSet = true;
// construct based on the children
std::vector<Node> children;
- const Datatype& dt = d_tn.getDatatype();
+ const DType& dt = d_tn.getDType();
Assert(d_consNum > 0 && d_consNum <= d_ccCons.size());
// get the current constructor number
unsigned cnum = d_ccCons[d_consNum - 1];
- children.push_back(Node::fromExpr(dt[cnum].getConstructor()));
+ children.push_back(dt[cnum].getConstructor());
// add the current of each child to children
for (unsigned i = 0, nargs = dt[cnum].getNumArgs(); i < nargs; i++)
{
TypeNode tn = n[0].getType();
// since n[0] is an evaluation head, we know tn is a sygus datatype
Assert(tn.isDatatype());
- const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+ const DType& dt = tn.getDType();
Assert(dt.isSygus());
if (n[0].getKind() == APPLY_CONSTRUCTOR)
{
}
// register this evaluation term with its head
d_evals[n[0]].push_back(n);
- Node var_list = Node::fromExpr(dt.getSygusVarList());
+ Node var_list = dt.getSygusVarList();
d_eval_args[n[0]].push_back(std::vector<Node>());
for (unsigned j = 1, size = n.getNumChildren(); j < size; j++)
{
bool hasSymCons = sti.hasSubtermSymbolicCons();
// n occurs as an evaluation head, thus it has sygus datatype type
Assert(tn.isDatatype());
- const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+ const DType& dt = tn.getDType();
Assert(dt.isSygus());
Trace("sygus-eval-unfold")
<< "SygusEvalUnfold: Register model value : " << vn << " for " << n
Node bTerm = d_tds->sygusToBuiltin(vn, tn);
Trace("sygus-eval-unfold") << "Built-in term : " << bTerm << std::endl;
std::vector<Node> vars;
- Node var_list = Node::fromExpr(dt.getSygusVarList());
+ Node var_list = dt.getSygusVarList();
for (const Node& v : var_list)
{
vars.push_back(v);
}
TypeNode headType = en[0].getType();
- Type headTypeT = headType.toType();
NodeManager* nm = NodeManager::currentNM();
- const Datatype& dt = headType.getDatatype();
+ const DType& dt = headType.getDType();
unsigned i = datatypes::utils::indexOf(ev.getOperator());
if (track_exp)
{
// explanation
- Node ee =
- nm->mkNode(APPLY_TESTER, Node::fromExpr(dt[i].getTester()), en[0]);
+ Node ee = nm->mkNode(APPLY_TESTER, dt[i].getTester(), en[0]);
if (std::find(exp.begin(), exp.end(), ee) == exp.end())
{
exp.push_back(ee);
}
}
// if we are a symbolic constructor, unfolding returns the subterm itself
- Node sop = Node::fromExpr(dt[i].getSygusOp());
+ Node sop = dt[i].getSygusOp();
if (sop.getAttribute(SygusAnyConstAttribute()))
{
Trace("sygus-eval-unfold-debug")
else
{
Node ret = nm->mkNode(
- APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(headTypeT, 0), en[0]);
+ APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(headType, 0), en[0]);
Trace("sygus-eval-unfold-debug")
<< "...return (from constructor) " << ret << std::endl;
return ret;
else
{
s = nm->mkNode(
- APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(headTypeT, j), en[0]);
+ APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(headType, j), en[0]);
}
cc.push_back(s);
if (track_exp)
#include "theory/quantifiers/sygus/sygus_explain.h"
+#include "expr/dtype.h"
#include "theory/datatypes/theory_datatypes_utils.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
return;
}
Assert(vn.getKind() == kind::APPLY_CONSTRUCTOR);
- const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype();
+ const DType& dt = tn.getDType();
int i = datatypes::utils::indexOf(vn.getOperator());
Node tst = datatypes::utils::mkTester(n, i, dt);
exp.push_back(tst);
if (cexc.find(j) == cexc.end())
{
Node sel = NodeManager::currentNM()->mkNode(
- kind::APPLY_SELECTOR_TOTAL,
- Node::fromExpr(dt[i].getSelectorInternal(tn.toType(), j)),
- n);
+ kind::APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(tn, j), n);
getExplanationForEquality(sel, vn[j], exp);
}
}
trb.replaceChild(i, vn[i]);
}
}
- const Datatype& dt = ((DatatypeType)ntn.toType()).getDatatype();
+ const DType& dt = ntn.getDType();
int cindex = datatypes::utils::indexOf(vn.getOperator());
Assert(cindex >= 0 && cindex < (int)dt.getNumConstructors());
Node tst = datatypes::utils::mkTester(n, cindex, dt);
for (unsigned i = 0; i < vn.getNumChildren(); i++)
{
Node sel = NodeManager::currentNM()->mkNode(
- kind::APPLY_SELECTOR_TOTAL,
- Node::fromExpr(dt[cindex].getSelectorInternal(ntn.toType(), i)),
- n);
+ kind::APPLY_SELECTOR_TOTAL, dt[cindex].getSelectorInternal(ntn, i), n);
Node vnr_c = vnr.isNull() ? vnr : (vn[i] == vnr[i] ? Node::null() : vnr[i]);
if (cexc.find(i) == cexc.end())
{
#include "theory/quantifiers/sygus/sygus_grammar_red.h"
+#include "expr/dtype.h"
#include "expr/sygus_datatype.h"
#include "options/quantifiers_options.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
Assert(tn.isDatatype());
TermDbSygus* tds = qe->getTermDatabaseSygus();
tds->registerSygusType(tn);
- const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+ const DType& dt = tn.getDType();
Assert(dt.isSygus());
- TypeNode btn = TypeNode::fromType(dt.getSygusType());
+ TypeNode btn = dt.getSygusType();
for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
{
Trace("sygus-red") << " Is " << dt[i].getName() << " a redundant operator?"
<< std::endl;
- Node sop = Node::fromExpr(dt[i].getSygusOp());
+ Node sop = dt[i].getSygusOp();
if (sop.getAttribute(SygusAnyConstAttribute()))
{
// the any constant constructor is never redundant
void SygusRedundantCons::getRedundant(std::vector<unsigned>& indices)
{
- const Datatype& dt = static_cast<DatatypeType>(d_type.toType()).getDatatype();
+ const DType& dt = d_type.getDType();
for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
{
if (isRedundant(i))
}
void SygusRedundantCons::getGenericList(TermDbSygus* tds,
- const Datatype& dt,
+ const DType& dt,
unsigned c,
unsigned index,
std::map<int, Node>& pre,
* to terms.
*/
void getGenericList(TermDbSygus* tds,
- const Datatype& dt,
+ const DType& dt,
unsigned c,
unsigned index,
std::map<int, Node>& pre,
// "any constant" constructors
return;
}
- const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+ const DType& dt = tn.getDType();
if (!dt.isSygus())
{
// may have recursed to a non-sygus-datatype
}
for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
{
- const DatatypeConstructor& dtc = dt[i];
+ const DTypeConstructor& dtc = dt[i];
// recurse on all subfields
for (unsigned j = 0, nargs = dtc.getNumArgs(); j < nargs; j++)
{
}
TypeNode tn = n.getType();
Assert(tn.isDatatype());
- const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+ const DType& dt = tn.getDType();
if (!dt.isSygus())
{
return false;
}
Node op = n.getOperator();
unsigned cindex = datatypes::utils::indexOf(op);
- Node sygusOp = Node::fromExpr(dt[cindex].getSygusOp());
+ Node sygusOp = dt[cindex].getSygusOp();
if (sygusOp.getAttribute(SygusAnyConstAttribute()))
{
// if it represents "any constant" then it is repairable
#include "theory/quantifiers/sygus/sygus_unif_strat.h"
+#include "expr/dtype.h"
#include "theory/datatypes/theory_datatypes_utils.h"
#include "theory/quantifiers/sygus/sygus_eval_unfold.h"
#include "theory/quantifiers/sygus/sygus_unif.h"
if (d_einfo.find(et) == d_einfo.end())
{
Trace("sygus-unif-debug")
- << "...register " << et << " for "
- << static_cast<DatatypeType>(tn.toType()).getDatatype().getName();
+ << "...register " << et << " for " << tn.getDType().getName();
Trace("sygus-unif-debug") << ", role = " << enum_role
<< ", in search = " << inSearch << std::endl;
d_einfo[et].initialize(enum_role);
ee = nm->mkSkolem("ee", tn);
eti.d_enum[erole] = ee;
Trace("sygus-unif-debug")
- << "...enumerator " << ee << " for "
- << static_cast<DatatypeType>(tn.toType()).getDatatype().getName()
+ << "...enumerator " << ee << " for " << tn.getDType().getName()
<< ", role = " << erole << std::endl;
}
else
// we know this is a sygus datatype since it is either the top-level type
// in the strategy graph, or was recursed by a strategy we inferred.
Assert(tn.isDatatype());
- const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+ const DType& dt = tn.getDType();
Assert(dt.isSygus());
std::map<Node, std::vector<StrategyType> > cop_to_strat;
bool search_this = false;
for (unsigned j = 0, ncons = dt.getNumConstructors(); j < ncons; j++)
{
- Node cop = Node::fromExpr(dt[j].getConstructor());
- Node op = Node::fromExpr(dt[j].getSygusOp());
+ Node cop = dt[j].getConstructor();
+ Node op = dt[j].getSygusOp();
Trace("sygus-unif-debug") << "--- Infer strategy from " << cop
<< " with sygus op " << op << "..." << std::endl;
std::vector<TypeNode> sktns;
for (unsigned k = 0, nargs = dt[j].getNumArgs(); k < nargs; k++)
{
- Type t = dt[j][k].getRangeType();
- TypeNode ttn = TypeNode::fromType(t);
+ TypeNode ttn = dt[j][k].getRangeType();
Node kv = nm->mkSkolem("ut", ttn);
sks.push_back(kv);
cop_to_sks[cop].push_back(kv);
Node ut = nm->mkNode(APPLY_CONSTRUCTOR, utchildren);
std::vector<Node> echildren;
echildren.push_back(ut);
- Node sbvl = Node::fromExpr(dt.getSygusVarList());
+ Node sbvl = dt.getSygusVarList();
for (const Node& sbv : sbvl)
{
echildren.push_back(sbv);
for (unsigned k = 0, size = cop_to_carg_list[cop].size(); k < size; k++)
{
TypeNode ctn = sktns[cop_to_carg_list[cop][k]];
- Trace("sygus-unif-debug")
- << " Child type " << k << " : "
- << static_cast<DatatypeType>(ctn.toType()).getDatatype().getName()
- << std::endl;
+ Trace("sygus-unif-debug") << " Child type " << k << " : "
+ << ctn.getDType().getName() << std::endl;
cop_to_child_types[cop].push_back(ctn);
}
// if there are checks on the consistency of child types wrt strategies,
{
// it is templated, allocate a fresh variable
et = nm->mkSkolem("et", ct);
- Trace("sygus-unif-debug")
- << "...enumerate " << et << " of type "
- << ((DatatypeType)ct.toType()).getDatatype().getName();
+ Trace("sygus-unif-debug") << "...enumerate " << et << " of type "
+ << ct.getDType().getName();
Trace("sygus-unif-debug") << " for arg " << j << " of "
- << static_cast<DatatypeType>(tn.toType())
- .getDatatype()
- .getName()
- << std::endl;
+ << tn.getDType().getName() << std::endl;
registerStrategyPoint(et, ct, erole_c, true);
d_einfo[et].d_template = cop_to_child_templ[cop][j];
d_einfo[et].d_template_arg = cop_to_child_templ_arg[cop][j];
else
{
Trace("sygus-unif-debug")
- << "...child type enumerate "
- << ((DatatypeType)ct.toType()).getDatatype().getName()
+ << "...child type enumerate " << ct.getDType().getName()
<< ", node role = " << nrole_c << std::endl;
// otherwise use the previous
Assert(d_tinfo[ct].d_enum.find(erole_c)
{
Trace("sygus-unif") << "Initialized strategy " << strat;
Trace("sygus-unif")
- << " for "
- << static_cast<DatatypeType>(tn.toType()).getDatatype().getName()
- << ", operator " << cop;
+ << " for " << tn.getDType().getName() << ", operator " << cop;
Trace("sygus-unif") << ", #children = " << cons_strat->d_cenum.size()
<< ", solution template = (lambda ( ";
for (const Node& targ : cons_strat->d_sol_templ_args)
std::map<Node, EnumInfo>::iterator itn = d_einfo.find(e);
Assert(itn != d_einfo.end());
// see if there is anything we can eliminate
- Trace("sygus-unif")
- << "* Search enumerator #" << i << " : type "
- << ((DatatypeType)e.getType().toType()).getDatatype().getName()
- << " : ";
+ Trace("sygus-unif") << "* Search enumerator #" << i << " : type "
+ << e.getType().getDType().getName() << " : ";
Trace("sygus-unif") << e << " has " << itn->second.d_enum_slave.size()
<< " slaves:" << std::endl;
for (unsigned j = 0; j < itn->second.d_enum_slave.size(); j++)
for (std::pair<const Node, std::map<unsigned, bool> >& nce : needs_cons)
{
Node em = nce.first;
- const Datatype& dt =
- static_cast<DatatypeType>(em.getType().toType()).getDatatype();
+ const DType& dt = em.getType().getDType();
std::vector<Node> lemmas;
for (std::pair<const unsigned, bool>& nc : nce.second)
{
// arguments of ITE are the same BOOL type
if (restrictions.d_iteReturnBoolConst)
{
- const Datatype& dt =
- static_cast<DatatypeType>(etn.toType()).getDatatype();
- Node op = Node::fromExpr(dt[cindex].getSygusOp());
- TypeNode sygus_tn = TypeNode::fromType(dt.getSygusType());
+ const DType& dt = etn.getDType();
+ Node op = dt[cindex].getSygusOp();
+ TypeNode sygus_tn = dt.getSygusType();
if (op.getKind() == kind::BUILTIN
- && NodeManager::operatorToKind(op) == ITE
- && sygus_tn.isBoolean()
- && (TypeNode::fromType(dt[cindex].getArgType(1))
- == TypeNode::fromType(dt[cindex].getArgType(2))))
+ && NodeManager::operatorToKind(op) == ITE && sygus_tn.isBoolean()
+ && (dt[cindex].getArgType(1) == dt[cindex].getArgType(2)))
{
unsigned ncons = dt.getNumConstructors(), indexT = ncons,
indexF = ncons;
for (unsigned k = 0; k < ncons; ++k)
{
- Node op_arg = Node::fromExpr(dt[k].getSygusOp());
+ Node op_arg = dt[k].getSygusOp();
if (dt[k].getNumArgs() > 0 || !op_arg.isConst())
{
continue;
}
}
// get the current datatype
- const Datatype& dt = static_cast<DatatypeType>(etn.toType()).getDatatype();
+ const DType& dt = etn.getDType();
// do not use recursive Boolean connectives for conditions of ITEs
if (nrole == role_ite_condition && restrictions.d_iteCondOnlyAtoms)
{
- TypeNode sygus_tn = TypeNode::fromType(dt.getSygusType());
+ TypeNode sygus_tn = dt.getSygusType();
for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++)
{
- Node op = Node::fromExpr(dt[j].getSygusOp());
+ Node op = dt[j].getSygusOp();
Trace("sygus-strat-slearn")
<< "...for ite condition, look at operator : " << op << std::endl;
if (op.isConst() && dt[j].getNumArgs() == 0)
bool type_ok = true;
for (unsigned k = 0, nargs = dt[j].getNumArgs(); k < nargs; k++)
{
- TypeNode tn = TypeNode::fromType(dt[j].getArgType(k));
+ TypeNode tn = dt[j].getArgType(k);
if (tn != etn)
{
type_ok = false;
indent(c, ind);
Trace(c) << e << " :: node role : " << nrole;
- Trace(c) << ", type : "
- << static_cast<DatatypeType>(etn.toType()).getDatatype().getName();
+ Trace(c) << ", type : " << etn.getDType().getName();
if (ei.isConditional())
{
Trace(c) << ", conditional";
Node prog = d_embed_quant[0][i];
int status = statuses[i];
TypeNode tn = prog.getType();
- const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+ const DType& dt = tn.getDType();
std::stringstream ss;
ss << prog;
std::string f(ss.str());
// pvs stores the variables that will be printed in the argument list
// below.
std::vector<Node> pvs;
- Node vl = Node::fromExpr(dt.getSygusVarList());
+ Node vl = dt.getSygusVarList();
if (!vl.isNull())
{
Assert(vl.getKind() == BOUND_VAR_LIST);
}
// convert to lambda
TypeNode tn = d_embed_quant[0][i].getType();
- const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+ const DType& dt = tn.getDType();
Node fvar = d_quant[0][i];
- Node bvl = Node::fromExpr(dt.getSygusVarList());
+ Node bvl = dt.getSygusVarList();
if (!bvl.isNull())
{
// since we don't have function subtyping, this assertion should only
TypeNode vtn = tn;
if( useSygusType ){
if( tn.isDatatype() ){
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ const DType& dt = tn.getDType();
if( !dt.getSygusType().isNull() ){
- vtn = TypeNode::fromType( dt.getSygusType() );
+ vtn = dt.getSygusType();
sindex = 1;
}
}
while( i>=(int)d_fv[sindex][tn].size() ){
std::stringstream ss;
if( tn.isDatatype() ){
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ const DType& dt = tn.getDType();
ss << "fv_" << dt.getName() << "_" << i;
}else{
ss << "fv_" << tn << "_" << i;
Node TermDbSygus::getProxyVariable(TypeNode tn, Node c)
{
Assert(tn.isDatatype());
- Assert(static_cast<DatatypeType>(tn.toType()).getDatatype().isSygus());
- Assert(
- TypeNode::fromType(
- static_cast<DatatypeType>(tn.toType()).getDatatype().getSygusType())
- .isComparableTo(c.getType()));
+ Assert(tn.getDType().isSygus());
+ Assert(tn.getDType().getSygusType().isComparableTo(c.getType()));
std::map<Node, Node>::iterator it = d_proxy_vars[tn].find(c);
if (it == d_proxy_vars[tn].end())
}
else
{
- const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+ const DType& dt = tn.getDType();
k = NodeManager::currentNM()->mkNode(
- APPLY_CONSTRUCTOR, Node::fromExpr(dt[anyC].getConstructor()), c);
+ APPLY_CONSTRUCTOR, dt[anyC].getConstructor(), c);
}
d_proxy_vars[tn][c] = k;
return k;
return d_fv_stype[v];
}
-Node TermDbSygus::mkGeneric(const Datatype& dt,
+Node TermDbSygus::mkGeneric(const DType& dt,
unsigned c,
std::map<TypeNode, int>& var_count,
std::map<int, Node>& pre,
a = it->second;
Trace("sygus-db-debug") << "From pre: " << a << std::endl;
}else{
- TypeNode tna = TypeNode::fromType(dt[c].getArgType(i));
+ TypeNode tna = dt[c].getArgType(i);
a = getFreeVarInc( tna, var_count, true );
}
Trace("sygus-db-debug")
return ret;
}
-Node TermDbSygus::mkGeneric(const Datatype& dt,
+Node TermDbSygus::mkGeneric(const DType& dt,
int c,
std::map<int, Node>& pre,
bool doBetaRed)
return mkGeneric(dt, c, var_count, pre, doBetaRed);
}
-Node TermDbSygus::mkGeneric(const Datatype& dt, int c, bool doBetaRed)
+Node TermDbSygus::mkGeneric(const DType& dt, int c, bool doBetaRed)
{
std::map<int, Node> pre;
return mkGeneric(dt, c, pre, doBetaRed);
}
Trace("sygus-db-debug") << "SygusToBuiltin : compute for " << n
<< ", type = " << tn << std::endl;
- const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+ const DType& dt = tn.getDType();
if (!dt.isSygus())
{
return n;
std::map<int, Node> pre;
for (unsigned j = 0, size = n.getNumChildren(); j < size; j++)
{
- pre[j] = sygusToBuiltin(n[j], TypeNode::fromType(dt[i].getArgType(j)));
+ pre[j] = sygusToBuiltin(n[j], dt[i].getArgType(j));
Trace("sygus-db-debug")
<< "sygus to builtin " << n[j] << " is " << pre[j] << std::endl;
}
// map to builtin variable type
int fv_num = getVarNum(n);
Assert(!dt.getSygusType().isNull());
- TypeNode vtn = TypeNode::fromType(dt.getSygusType());
+ TypeNode vtn = dt.getSygusType();
Node ret = getFreeVar(vtn, fv_num);
return ret;
}
{
sum += getSygusTermSize(n[i]);
}
- const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr());
+ const DType& dt = datatypes::utils::datatypeOf(n.getOperator());
int cindex = datatypes::utils::indexOf(n.getOperator());
Assert(cindex >= 0 && cindex < (int)dt.getNumConstructors());
unsigned weight = dt[cindex].getWeight();
{
return false;
}
- const Datatype& dt = tn.getDatatype();
+ const DType& dt = tn.getDType();
if (!dt.isSygus())
{
return false;
TypeNode stn = sf_types[i];
Assert(stn.isDatatype());
SygusTypeInfo& sti = getTypeInfo(stn);
- const Datatype& dt = stn.getDatatype();
+ const DType& dt = stn.getDType();
int anyC = sti.getAnyConstantConsNum();
for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
{
- Expr sop = dt[i].getSygusOp();
- Assert(!sop.isNull());
bool isAnyC = static_cast<int>(i) == anyC;
if (isAnyC && !useSymbolicCons)
{
// sygus stream are to find many solutions to an easy problem, where
// the bottleneck often becomes the large number of "exclude the current
// solution" clauses.
- const Datatype& dt = et.getDatatype();
+ const DType& dt = et.getDType();
if (options::sygusStream()
|| (!eti.hasIte() && !dt.getSygusType().isBoolean()))
{
{
d_sel_weight[tn].clear();
itsw = d_sel_weight.find(tn);
- Type t = tn.toType();
- const Datatype& dt = static_cast<DatatypeType>(t).getDatatype();
+ const DType& dt = tn.getDType();
Trace("sygus-db") << "Compute selector weights for " << dt.getName()
<< std::endl;
for (unsigned i = 0, size = dt.getNumConstructors(); i < size; i++)
unsigned cw = dt[i].getWeight();
for (unsigned j = 0, size2 = dt[i].getNumArgs(); j < size2; j++)
{
- Node csel = Node::fromExpr(dt[i].getSelectorInternal(t, j));
+ Node csel = dt[i].getSelectorInternal(tn, j);
std::map<Node, unsigned>::iterator its = itsw->second.find(csel);
if (its == itsw->second.end() || cw < its->second)
{
return itsw->second[sel];
}
-TypeNode TermDbSygus::getArgType(const DatatypeConstructor& c, unsigned i) const
+TypeNode TermDbSygus::getArgType(const DTypeConstructor& c, unsigned i) const
{
Assert(i < c.getNumArgs());
- return TypeNode::fromType(
- static_cast<SelectorType>(c[i].getType()).getRangeType());
+ return c.getArgType(i);
}
-bool TermDbSygus::isTypeMatch( const DatatypeConstructor& c1, const DatatypeConstructor& c2 ) {
+bool TermDbSygus::isTypeMatch(const DTypeConstructor& c1,
+ const DTypeConstructor& c2)
+{
if( c1.getNumArgs()!=c2.getNumArgs() ){
return false;
}else{
}
TypeNode tn = n.getType();
Assert(tn.isDatatype());
- const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+ const DType& dt = tn.getDType();
Assert(dt.isSygus());
unsigned cindex = datatypes::utils::indexOf(n.getOperator());
- Node sygusOp = Node::fromExpr(dt[cindex].getSygusOp());
+ Node sygusOp = dt[cindex].getSygusOp();
// it is symbolic if it represents "any constant"
return sygusOp.getAttribute(SygusAnyConstAttribute());
}
Assert(isRegistered(tn));
SygusTypeInfo& ti = getTypeInfo(tn);
int c = ti.getKindConsNum(k);
- const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+ const DType& dt = tn.getDType();
if (c != -1)
{
for (unsigned i = 0, nargs = dt[c].getNumArgs(); i < nargs; i++)
{
- argts.push_back(TypeNode::fromType(dt[c].getArgType(i)));
+ argts.push_back(dt[c].getArgType(i));
}
return true;
}
#include <unordered_set>
+#include "expr/dtype.h"
#include "theory/evaluator.h"
#include "theory/quantifiers/extended_rewrite.h"
#include "theory/quantifiers/fun_def_evaluator.h"
* If doBetaRed is true, then lambda operators are eagerly eliminated via
* beta reduction.
*/
- Node mkGeneric(const Datatype& dt,
+ Node mkGeneric(const DType& dt,
unsigned c,
std::map<TypeNode, int>& var_count,
std::map<int, Node>& pre,
bool doBetaRed = true);
/** same as above, but with empty var_count */
- Node mkGeneric(const Datatype& dt,
+ Node mkGeneric(const DType& dt,
int c,
std::map<int, Node>& pre,
bool doBetaRed = true);
/** same as above, but with empty pre */
- Node mkGeneric(const Datatype& dt, int c, bool doBetaRed = true);
+ Node mkGeneric(const DType& dt, int c, bool doBetaRed = true);
/** makes a symbolic term concrete
*
* Given a sygus datatype term n of type tn with holes (symbolic constructor
/** get the weight of the selector, where tn is the domain of sel */
unsigned getSelectorWeight(TypeNode tn, Node sel);
/** get arg type */
- TypeNode getArgType(const DatatypeConstructor& c, unsigned i) const;
+ TypeNode getArgType(const DTypeConstructor& c, unsigned i) const;
/** Do constructors c1 and c2 have the same type? */
- bool isTypeMatch( const DatatypeConstructor& c1, const DatatypeConstructor& c2 );
+ bool isTypeMatch(const DTypeConstructor& c1, const DTypeConstructor& c2);
/** return whether n is an application of a symbolic constructor */
bool isSymbolicConsApp(Node n) const;
/** can construct kind
#include "theory/quantifiers/sygus/type_info.h"
#include "base/check.h"
+#include "expr/dtype.h"
#include "expr/sygus_datatype.h"
#include "theory/datatypes/theory_datatypes_utils.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
{
d_this = tn;
Assert(tn.isDatatype());
- const Datatype& dt = tn.getDatatype();
+ const DType& dt = tn.getDType();
Assert(dt.isSygus());
Trace("sygus-db") << "Register type " << dt.getName() << "..." << std::endl;
- TypeNode btn = TypeNode::fromType(dt.getSygusType());
+ TypeNode btn = dt.getSygusType();
d_btype = btn;
Assert(!d_btype.isNull());
// get the sygus variable list
- Node var_list = Node::fromExpr(dt.getSygusVarList());
+ Node var_list = dt.getSygusVarList();
if (!var_list.isNull())
{
for (unsigned j = 0; j < var_list.getNumChildren(); j++)
{
for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
{
- TypeNode ctn = TypeNode::fromType(dt[i].getArgType(j));
+ TypeNode ctn = dt[i].getArgType(j);
Trace("sygus-db") << " register subfield type " << ctn << std::endl;
if (tds->registerSygusType(ctn))
{
// iterate over constructors
for (unsigned i = 0; i < dt.getNumConstructors(); i++)
{
- Expr sop = dt[i].getSygusOp();
+ Node sop = dt[i].getSygusOp();
Assert(!sop.isNull());
- Node n = Node::fromExpr(sop);
Trace("sygus-db") << " Operator #" << i << " : " << sop;
if (sop.getKind() == kind::BUILTIN)
{
- Kind sk = NodeManager::operatorToKind(n);
+ Kind sk = NodeManager::operatorToKind(sop);
Trace("sygus-db") << ", kind = " << sk;
d_kinds[sk] = i;
d_arg_kind[i] = sk;
else if (sop.isConst() && dt[i].getNumArgs() == 0)
{
Trace("sygus-db") << ", constant";
- d_consts[n] = i;
- d_arg_const[i] = n;
+ d_consts[sop] = i;
+ d_arg_const[i] = sop;
}
else if (sop.getKind() == LAMBDA)
{
Assert(sop[0].getNumChildren() == dt[i].getNumArgs());
for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
{
- TypeNode ct = TypeNode::fromType(dt[i].getArgType(j));
+ TypeNode ct = dt[i].getArgType(j);
TypeNode cbt = tds->sygusToBuiltinType(ct);
- TypeNode lat = TypeNode::fromType(sop[0][j].getType());
+ TypeNode lat = sop[0][j].getType();
AlwaysAssert(cbt.isSubtypeOf(lat))
<< "In sygus datatype " << dt.getName()
<< ", argument to a lambda constructor is not " << lat << std::endl;
}
}
// symbolic constructors
- if (n.getAttribute(SygusAnyConstAttribute()))
+ if (sop.getAttribute(SygusAnyConstAttribute()))
{
d_sym_cons_any_constant = i;
d_has_subterm_sym_cons = true;
}
- d_ops[n] = i;
- d_arg_ops[i] = n;
+ d_ops[sop] = i;
+ d_arg_ops[i] = sop;
Trace("sygus-db") << std::endl;
// We must properly catch type errors in sygus grammars for arguments of
// builtin operators. The challenge is that we easily ask for expected
csize = 1;
for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
{
- TypeNode ct = TypeNode::fromType(dt[i].getArgType(j));
+ TypeNode ct = dt[i].getArgType(j);
if (ct == tn)
{
csize += d_min_term_size;
}
else
{
- Assert(!ct.isDatatype() || !ct.getDatatype().isSygus());
+ Assert(!ct.isDatatype() || !ct.getDType().isSygus());
}
}
}
std::vector<unsigned> rm_indices;
TypeNode stn = sf_types[i];
Assert(stn.isDatatype());
- const Datatype& dt = stn.getDatatype();
+ const DType& dt = stn.getDType();
for (unsigned j = 0, ncons = dt.getNumConstructors(); j < ncons; j++)
{
- Expr sop = dt[j].getSygusOp();
- Assert(!sop.isNull());
- Node sopn = Node::fromExpr(sop);
+ Node sopn = dt[j].getSygusOp();
+ Assert(!sopn.isNull());
if (type_occurs.find(sopn) != type_occurs.end())
{
// if it is a variable, store that it occurs in stn
// do not recurse to non-datatype types
return;
}
- const Datatype& dt = tn.getDatatype();
+ const DType& dt = tn.getDType();
if (!dt.isSygus())
{
// do not recurse to non-sygus datatype types
{
for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
{
- TypeNode at = TypeNode::fromType(dt[i].getArgType(j));
+ TypeNode at = dt[i].getArgType(j);
computeMinTypeDepthInternal(at, type_depth + 1);
}
}
#include "theory/quantifiers/sygus_sampler.h"
+#include "expr/dtype.h"
#include "expr/node_algorithm.h"
#include "options/base_options.h"
#include "options/quantifiers_options.h"
d_is_valid = true;
d_ftn = f.getType();
Assert(d_ftn.isDatatype());
- const Datatype& dt = static_cast<DatatypeType>(d_ftn.toType()).getDatatype();
+ const DType& dt = d_ftn.getDType();
Assert(dt.isSygus());
Trace("sygus-sample") << "Register sampler for " << f << std::endl;
d_rvalue_null_cindices.clear();
d_var_sygus_types.clear();
// get the sygus variable list
- Node var_list = Node::fromExpr(dt.getSygusVarList());
+ Node var_list = dt.getSygusVarList();
if (!var_list.isNull())
{
for (const Node& sv : var_list)
{
return getRandomValue(tn);
}
- const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+ const DType& dt = tn.getDType();
if (!dt.isSygus())
{
return getRandomValue(tn);
<< "Recurse constructor index #" << index << std::endl;
unsigned cindex = cindices[index];
Assert(cindex < dt.getNumConstructors());
- const DatatypeConstructor& dtc = dt[cindex];
+ const DTypeConstructor& dtc = dt[cindex];
// more likely to terminate in recursive calls
double rchance_new = rchance + (1.0 - rchance) * rinc;
std::map<int, Node> pre;
}
Trace("sygus-sample-grammar") << "...resort to random value" << std::endl;
// if we did not generate based on the grammar, pick a random value
- return getRandomValue(TypeNode::fromType(dt.getSygusType()));
+ return getRandomValue(dt.getSygusType());
}
// recursion depth bounded by number of types in grammar (small)
{
return;
}
- const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+ const DType& dt = tn.getDType();
if (!dt.isSygus())
{
return;
}
for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
{
- const DatatypeConstructor& dtc = dt[i];
- Node sop = Node::fromExpr(dtc.getSygusOp());
+ const DTypeConstructor& dtc = dt[i];
+ Node sop = dtc.getSygusOp();
bool isVar = std::find(d_vars.begin(), d_vars.end(), sop) != d_vars.end();
if (isVar)
{
#ifndef SRC_THEORY_SETS_RELS_UTILS_H_
#define SRC_THEORY_SETS_RELS_UTILS_H_
+#include "expr/dtype.h"
+#include "expr/node.h"
+
namespace CVC4 {
namespace theory {
namespace sets {
return tuple[n_th];
}
TypeNode tn = tuple.getType();
- const Datatype& dt = tn.getDatatype();
- return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal( tn.toType(), n_th ), tuple);
+ const DType& dt = tn.getDType();
+ return NodeManager::currentNM()->mkNode(
+ kind::APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal(tn, n_th), tuple);
}
static Node reverseTuple( Node tuple ) {
std::vector<TypeNode> tuple_types = tuple.getType().getTupleTypes();
std::reverse( tuple_types.begin(), tuple_types.end() );
TypeNode tn = NodeManager::currentNM()->mkTupleType( tuple_types );
- const Datatype& dt = tn.getDatatype();
- elements.push_back( Node::fromExpr(dt[0].getConstructor() ) );
+ const DType& dt = tn.getDType();
+ elements.push_back(dt[0].getConstructor());
for(int i = tuple_types.size() - 1; i >= 0; --i) {
elements.push_back( nthElementOfTuple(tuple, i) );
}
return NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, elements );
}
static Node constructPair(Node rel, Node a, Node b) {
- const Datatype& dt = rel.getType().getSetElementType().getDatatype();
- return NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt[0].getConstructor()), a, b);
+ const DType& dt = rel.getType().getSetElementType().getDType();
+ return NodeManager::currentNM()->mkNode(
+ kind::APPLY_CONSTRUCTOR, dt[0].getConstructor(), a, b);
}
};
}
hasChecked.insert( fst_mem_rep );
- const Datatype& dt =
- join_image_term.getType().getSetElementType().getDatatype();
- Node new_membership = NodeManager::currentNM()->mkNode(kind::MEMBER,
- NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR,
- Node::fromExpr(dt[0].getConstructor()), fst_mem_rep ),
- join_image_term);
+ const DType& dt =
+ join_image_term.getType().getSetElementType().getDType();
+ Node new_membership = nm->mkNode(
+ MEMBER,
+ nm->mkNode(APPLY_CONSTRUCTOR, dt[0].getConstructor(), fst_mem_rep),
+ join_image_term);
if (d_state.isEntailed(new_membership, true))
{
++mem_rep_it;
Node reason = exp;
Node fst_mem = RelsUtils::nthElementOfTuple( exp[0], 0 );
Node snd_mem = RelsUtils::nthElementOfTuple( exp[0], 1 );
- const Datatype& dt =
- iden_term[0].getType().getSetElementType().getDatatype();
- Node fact = NodeManager::currentNM()->mkNode( kind::MEMBER, NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt[0].getConstructor()), fst_mem ), iden_term[0] );
+ const DType& dt = iden_term[0].getType().getSetElementType().getDType();
+ Node fact = nm->mkNode(
+ MEMBER,
+ nm->mkNode(APPLY_CONSTRUCTOR, dt[0].getConstructor(), fst_mem),
+ iden_term[0]);
if( exp[1] != iden_term ) {
reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode( kind::EQUAL, exp[1], iden_term ) );
Node mem = exp[0];
std::vector<Node> r1_element;
std::vector<Node> r2_element;
- const Datatype& dt1 = pt_rel[0].getType().getSetElementType().getDatatype();
+ const DType& dt1 = pt_rel[0].getType().getSetElementType().getDType();
unsigned int s1_len = pt_rel[0].getType().getSetElementType().getTupleLength();
unsigned int tup_len = pt_rel.getType().getSetElementType().getTupleLength();
- r1_element.push_back(Node::fromExpr(dt1[0].getConstructor()));
+ r1_element.push_back(dt1[0].getConstructor());
unsigned int i = 0;
for(; i < s1_len; ++i) {
r1_element.push_back(RelsUtils::nthElementOfTuple(mem, i));
}
- const Datatype& dt2 = pt_rel[1].getType().getSetElementType().getDatatype();
- r2_element.push_back(Node::fromExpr(dt2[0].getConstructor()));
+ const DType& dt2 = pt_rel[1].getType().getSetElementType().getDType();
+ r2_element.push_back(dt2[0].getConstructor());
for(; i < tup_len; ++i) {
r2_element.push_back(RelsUtils::nthElementOfTuple(mem, i));
}
TypeNode shared_type = r2_rep.getType().getSetElementType().getTupleTypes()[0];
Node shared_x = d_state.getSkolemCache().mkTypedSkolemCached(
shared_type, mem, join_rel, SkolemCache::SK_JOIN, "srj");
- const Datatype& dt1 =
- join_rel[0].getType().getSetElementType().getDatatype();
+ const DType& dt1 = join_rel[0].getType().getSetElementType().getDType();
unsigned int s1_len = join_rel[0].getType().getSetElementType().getTupleLength();
unsigned int tup_len = join_rel.getType().getSetElementType().getTupleLength();
unsigned int i = 0;
- r1_element.push_back(Node::fromExpr(dt1[0].getConstructor()));
+ r1_element.push_back(dt1[0].getConstructor());
for(; i < s1_len-1; ++i) {
r1_element.push_back(RelsUtils::nthElementOfTuple(mem, i));
}
r1_element.push_back(shared_x);
- const Datatype& dt2 =
- join_rel[1].getType().getSetElementType().getDatatype();
- r2_element.push_back(Node::fromExpr(dt2[0].getConstructor()));
+ const DType& dt2 = join_rel[1].getType().getSetElementType().getDType();
+ r2_element.push_back(dt2[0].getConstructor());
r2_element.push_back(shared_x);
for(; i < tup_len; ++i) {
r2_element.push_back(RelsUtils::nthElementOfTuple(mem, i));
TypeNode tn = rel.getType().getSetElementType();
Node r1_rmost = RelsUtils::nthElementOfTuple( r1_rep_exps[i][0], r1_tuple_len-1 );
Node r2_lmost = RelsUtils::nthElementOfTuple( r2_rep_exps[j][0], 0 );
- tuple_elements.push_back( Node::fromExpr(tn.getDatatype()[0].getConstructor()) );
+ tuple_elements.push_back(tn.getDType()[0].getConstructor());
if( (areEqual(r1_rmost, r2_lmost) && rel.getKind() == kind::JOIN) ||
rel.getKind() == kind::PRODUCT ) {
if(d_symbolic_tuples.find(n) == d_symbolic_tuples.end()) {
Trace("rels-debug") << "[Theory::Rels] Reduce tuple var: " << n[0] << " to a concrete one " << " node = " << n << std::endl;
std::vector<Node> tuple_elements;
- tuple_elements.push_back(Node::fromExpr((n[0].getType().getDatatype())[0].getConstructor()));
+ tuple_elements.push_back((n[0].getType().getDType())[0].getConstructor());
for(unsigned int i = 0; i < n[0].getType().getTupleLength(); i++) {
Node element = RelsUtils::nthElementOfTuple(n[0], i);
makeSharedTerm(element);
#include "theory/sets/normal_form.h"
#include "theory/sets/rels_utils.h"
+using namespace CVC4::kind;
+
namespace CVC4 {
namespace theory {
namespace sets {
while(left_it != left.end()) {
Trace("rels-debug") << "Sets::postRewrite processing left_it = " << *left_it << std::endl;
std::vector<Node> left_tuple;
- left_tuple.push_back(Node::fromExpr(tn.getDatatype()[0].getConstructor()));
+ left_tuple.push_back(tn.getDType()[0].getConstructor());
for(int i = 0; i < left_len; i++) {
left_tuple.push_back(RelsUtils::nthElementOfTuple(*left_it,i));
}
TypeNode tn = node.getType().getSetElementType();
while(left_it != left.end()) {
std::vector<Node> left_tuple;
- left_tuple.push_back(Node::fromExpr(tn.getDatatype()[0].getConstructor()));
+ left_tuple.push_back(tn.getDType()[0].getConstructor());
for(int i = 0; i < left_len - 1; i++) {
left_tuple.push_back(RelsUtils::nthElementOfTuple(*left_it,i));
}
++rel_mems_it_snd;
}
if( existing_mems.size() >= min_card ) {
- const Datatype& dt = node.getType().getSetElementType().getDatatype();
- join_img_mems.insert(NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt[0].getConstructor()), fst_mem ));
+ const DType& dt = node.getType().getSetElementType().getDType();
+ join_img_mems.insert(
+ nm->mkNode(APPLY_CONSTRUCTOR, dt[0].getConstructor(), fst_mem));
}
++rel_mems_it;
}
**/
#include "theory/theory_model_builder.h"
+#include "expr/dtype.h"
#include "options/quantifiers_options.h"
#include "options/smt_options.h"
#include "options/uf_options.h"
}
else if (tn.isDatatype())
{
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ const DType& dt = tn.getDType();
return dt.involvesUninterpretedType();
}
else
}
else if (tn.isDatatype())
{
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ const DType& dt = tn.getDType();
for (unsigned i = 0; i < dt.getNumConstructors(); i++)
{
for (unsigned j = 0; j < dt[i].getNumArgs(); j++)
{
- TypeNode ctn = TypeNode::fromType(dt[i][j].getRangeType());
+ TypeNode ctn = dt[i][j].getRangeType();
addToTypeList(ctn, type_list, visiting);
}
}
bool isCorecursive = false;
if (t.isDatatype())
{
- const Datatype& dt = ((DatatypeType)(t).toType()).getDatatype();
- isCorecursive =
- dt.isCodatatype() && (!dt.isFinite(t.toType())
- || dt.isRecursiveSingleton(t.toType()));
+ const DType& dt = t.getDType();
+ isCorecursive = dt.isCodatatype()
+ && (!dt.isFinite(t) || dt.isRecursiveSingleton(t));
}
#ifdef CVC4_ASSERTIONS
bool isUSortFiniteRestricted = false;
projects / cvc5.git / commitdiff