Towards eliminating option scopes.
return (*this)[index].getType().getDatatypeSelectorRangeType();
}
-Node DTypeConstructor::getSelectorInternal(TypeNode domainType,
- size_t index) const
+Node DTypeConstructor::getSelector(size_t index) const
{
Assert(isResolved());
Assert(index < getNumArgs());
- if (options::dtSharedSelectors())
- {
- computeSharedSelectors(domainType);
- Assert(d_sharedSelectors[domainType].size() == getNumArgs());
- return d_sharedSelectors[domainType][index];
- }
- else
- {
- return d_args[index]->getSelector();
- }
+ return d_args[index]->getSelector();
+}
+
+Node DTypeConstructor::getSharedSelector(TypeNode domainType,
+ size_t index) const
+{
+ Assert(isResolved());
+ Assert(index < getNumArgs());
+ computeSharedSelectors(domainType);
+ Assert(d_sharedSelectors[domainType].size() == getNumArgs());
+ return d_sharedSelectors[domainType][index];
}
int DTypeConstructor::getSelectorIndexInternal(Node sel) const
/** get selector internal
*
- * This gets the selector for the index^th argument
- * of this constructor. The type dtt is the datatype
- * type whose datatype is the owner of this constructor,
- * where this type may be an instantiated parametric datatype.
- *
- * If shared selectors are enabled,
- * this returns a shared (constructor-agnotic) selector, which
+ * This gets the (unshared) selector for the index^th argument
+ * of this constructor.
+ */
+ Node getSelector(size_t index) const;
+ /**
+ * This returns a shared (constructor-agnotic) selector, which
* in the terminology of "DTypes with Shared Selectors", is:
* sel_{dtt}^{T,atos(T,C,index)}
* where C is this constructor, and T is the type
* type T of constructor term t if one exists, or is
* unconstrained otherwise.
*/
- Node getSelectorInternal(TypeNode dtt, size_t index) const;
+ Node getSharedSelector(TypeNode dtt, size_t index) const;
/** get selector index internal
*
namespace theory {
namespace datatypes {
-DatatypesRewriter::DatatypesRewriter(Evaluator* sygusEval)
- : d_sygusEval(sygusEval)
+DatatypesRewriter::DatatypesRewriter(Evaluator* sygusEval, const Options& opts)
+ : d_sygusEval(sygusEval), d_opts(opts)
{
}
return n;
}
-Node DatatypesRewriter::expandApplySelector(Node n)
+Node DatatypesRewriter::expandApplySelector(Node n, bool sharedSel)
{
Assert(n.getKind() == APPLY_SELECTOR);
Node selector = n.getOperator();
- if (!options::dtSharedSelectors()
- || !selector.hasAttribute(DTypeConsIndexAttr()))
+ if (!sharedSel || !selector.hasAttribute(DTypeConsIndexAttr()))
{
return n;
}
size_t selectorIndex = utils::indexOf(selector);
Trace("dt-expand") << "...selector index = " << selectorIndex << std::endl;
Assert(selectorIndex < c.getNumArgs());
- Node selector_use = c.getSelectorInternal(ndt, selectorIndex);
- NodeManager* nm = NodeManager::currentNM();
- Node sel = nm->mkNode(kind::APPLY_SELECTOR, selector_use, n[0]);
- return sel;
+ return utils::applySelector(c, selectorIndex, true, n[0]);
}
TrustNode DatatypesRewriter::expandDefinition(Node n)
{
case kind::APPLY_SELECTOR:
{
- ret = expandApplySelector(n);
+ ret = expandApplySelector(n, d_opts.datatypes.dtSharedSelectors);
}
break;
case APPLY_UPDATER:
Trace("dt-expand") << "expr is " << n << std::endl;
Trace("dt-expand") << "updateIndex is " << updateIndex << std::endl;
Trace("dt-expand") << "t is " << tn << std::endl;
+ bool shareSel = d_opts.datatypes.dtSharedSelectors;
for (size_t i = 0, size = dc.getNumArgs(); i < size; ++i)
{
if (i == updateIndex)
}
else
{
- b << nm->mkNode(APPLY_SELECTOR, dc.getSelectorInternal(tn, i), n[0]);
+ b << utils::applySelector(dc, i, shareSel, n[0]);
}
}
ret = b;
#include "theory/theory_rewriter.h"
namespace cvc5::internal {
+
+class Options;
+
namespace theory {
namespace datatypes {
class DatatypesRewriter : public TheoryRewriter
{
public:
- DatatypesRewriter(Evaluator* sygusEval);
+ DatatypesRewriter(Evaluator* sygusEval, const Options& opts);
RewriteResponse postRewrite(TNode in) override;
RewriteResponse preRewrite(TNode in) override;
* (APPLY_SELECTOR selC x)
* its expanded form is
* (APPLY_SELECTOR selC' x)
- * where f is a skolem function with id SELECTOR_WRONG, and selC' is the
- * internal selector function for selC (possibly a shared selector).
+ * where selC' is the internal selector function for selC (a shared selector
+ * if sharedSel is true).
* Note that we do not introduce an uninterpreted function here, e.g. to
* handle when the selector is misapplied. This is because it suffices to
* reason about the original selector term e.g. via congruence.
*/
- static Node expandApplySelector(Node n);
+ static Node expandApplySelector(Node n, bool sharedSel);
/**
* Expand a match term into its definition.
* For example
Node sygusToBuiltinEval(Node n, const std::vector<Node>& args);
/** Pointer to the evaluator, used as an optimization for the above method */
Evaluator* d_sygusEval;
+ /** Reference to the options */
+ const Options& d_opts;
};
} // namespace datatypes
return Node::null();
}
Node tester = utils::mkTester(t, i, dt);
- Node ticons = utils::getInstCons(t, dt, i);
+ Node ticons = utils::getInstCons(t, dt, i, d_sharedSel);
return tester.eqNode(t.eqNode(ticons));
}
else if (id == PfRule::DT_COLLAPSE)
class DatatypesProofRuleChecker : public ProofRuleChecker
{
public:
- DatatypesProofRuleChecker() {}
+ DatatypesProofRuleChecker(bool sharedSel) : d_sharedSel(sharedSel) {}
~DatatypesProofRuleChecker() {}
/** Register all rules owned by this rule checker into pc. */
Node checkInternal(PfRule id,
const std::vector<Node>& children,
const std::vector<Node>& args) override;
+ /** Whether we are using shared selectors */
+ bool d_sharedSel;
};
} // namespace datatypes
{
Trace("sygus-sb-debug") << "Do lazy symmetry breaking...\n";
for( unsigned j=0; j<dt[tindex].getNumArgs(); j++ ){
- Node sel =
- nm->mkNode(APPLY_SELECTOR, dt[tindex].getSelectorInternal(ntn, j), n);
+ Node sel = nm->mkNode(
+ APPLY_SELECTOR, getSelectorInternal(ntn, dt[tindex], 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 );
for (unsigned j = 0; j < dt_index_nargs; j++)
{
Node sel =
- nm->mkNode(APPLY_SELECTOR, dt[tindex].getSelectorInternal(tn, j), n);
+ nm->mkNode(APPLY_SELECTOR, getSelectorInternal(tn, dt[tindex], j), n);
Assert(sel.getType().isDatatype());
children.push_back(sel);
}
&& !isAnyConstant)
{
Node szl = nm->mkNode(DT_SIZE, n);
- Node szr = nm->mkNode(DT_SIZE, utils::getInstCons(n, dt, tindex));
+ Node szr =
+ nm->mkNode(DT_SIZE,
+ utils::getInstCons(
+ n, dt, tindex, options().datatypes.dtSharedSelectors));
szr = rewrite(szr);
sbp_conj.push_back(szl.eqNode(szr));
}
&& children[0].getType() == tn && children[1].getType() == tn)
{
// chainable
- Node child11 = nm->mkNode(
- APPLY_SELECTOR, dt[tindex].getSelectorInternal(tn, 1), children[0]);
+ Node child11 = nm->mkNode(APPLY_SELECTOR,
+ getSelectorInternal(tn, dt[tindex], 1),
+ children[0]);
Assert(child11.getType() == children[1].getType());
Node order_pred_trans =
nm->mkNode(OR,
for (unsigned i = 0, nchild = nv.getNumChildren(); i < nchild; i++)
{
Node sel =
- nm->mkNode(APPLY_SELECTOR, dt[cindex].getSelectorInternal(tn, i), n);
+ nm->mkNode(APPLY_SELECTOR, getSelectorInternal(tn, dt[cindex], i), n);
Node nvc = registerSearchValue(a,
sel,
nv[i],
}
for( unsigned i=0; i<vn.getNumChildren(); i++ ){
Node sel =
- nm->mkNode(APPLY_SELECTOR, dt[cindex].getSelectorInternal(tn, i), n);
+ nm->mkNode(APPLY_SELECTOR, getSelectorInternal(tn, dt[cindex], i), n);
if (!checkValue(sel, vn[i], ind + 1))
{
return false;
children.push_back(dt[tindex].getConstructor());
for( unsigned i=0; i<dt[tindex].getNumArgs(); i++ ){
Node sel = NodeManager::currentNM()->mkNode(
- APPLY_SELECTOR, dt[tindex].getSelectorInternal(tn, i), n);
+ APPLY_SELECTOR, getSelectorInternal(tn, dt[tindex], i), n);
Node cc = getCurrentTemplate( sel, var_count );
children.push_back( cc );
}
}
}
+Node SygusExtension::getSelectorInternal(TypeNode dtt,
+ const DTypeConstructor& dc,
+ size_t index) const
+{
+ return utils::getSelector(
+ dtt, dc, index, options().datatypes.dtSharedSelectors);
+}
* false, and 0 if it is not asserted.
*/
int getGuardStatus( Node g );
+ /** Calls util::getSelector based on the value of options::dtShareSel */
+ Node getSelectorInternal(TypeNode dtt,
+ const DTypeConstructor& dc,
+ size_t index) const;
};
}
d_functionTerms(context()),
d_singleton_eq(userContext()),
d_sygusExtension(nullptr),
- d_rewriter(env.getEvaluator()),
+ d_rewriter(env.getEvaluator(), env.getOptions()),
d_state(env, valuation),
d_im(env, *this, d_state),
d_notify(d_im, *this),
+ d_checker(env.getOptions().datatypes.dtSharedSelectors),
d_cpacb(*this)
{
//unsigned orig_size = nodes.size();
std::map< TypeNode, int > typ_enum_map;
std::vector< TypeEnumerator > typ_enum;
- unsigned index = 0;
- while( index<nodes.size() ){
+ size_t index = 0;
+ bool shareSel = options().datatypes.dtSharedSelectors;
+ while (index < nodes.size())
+ {
Node eqc = nodes[index];
Node neqc;
bool addCons = false;
Trace("dt-cmi") << pcons[i] << " ";
}
Trace("dt-cmi") << std::endl;
- for( unsigned r=0; r<2; r++ ){
+ for (size_t r = 0; r < 2; r++)
+ {
if( neqc.isNull() ){
- for( unsigned i=0; i<pcons.size(); i++ ){
+ for (size_t i = 0, psize = pcons.size(); i < psize; i++)
+ {
// must try the infinite ones first
bool cfinite =
d_env.isFiniteType(dt[i].getInstantiatedConstructorType(tt));
if( pcons[i] && (r==1)==cfinite ){
- neqc = utils::getInstCons(eqc, dt, i);
+ neqc = utils::getInstCons(eqc, dt, i, shareSel);
break;
}
}
}
//add constructor to equivalence class
Node k = getTermSkolemFor( n );
- Node n_ic = utils::getInstCons(k, dt, index);
+ Node n_ic =
+ utils::getInstCons(k, dt, index, options().datatypes.dtSharedSelectors);
Assert (n_ic == rewrite(n_ic));
Trace("dt-enum") << "Made instantiate cons " << n_ic << std::endl;
return n_ic;
#include "expr/dtype.h"
#include "expr/dtype_cons.h"
-using namespace cvc5::internal;
using namespace cvc5::internal::kind;
namespace cvc5::internal {
namespace datatypes {
namespace utils {
-/** get instantiate cons */
-Node getInstCons(Node n, const DType& dt, size_t index)
+Node getSelector(TypeNode dtt,
+ const DTypeConstructor& dc,
+ size_t index,
+ bool shareSel)
+{
+ return shareSel ? dc.getSharedSelector(dtt, index) : dc.getSelector(index);
+}
+
+Node applySelector(const DTypeConstructor& dc,
+ size_t index,
+ bool shareSel,
+ const Node& n)
+{
+ Node s = getSelector(n.getType(), dc, index, shareSel);
+ return NodeManager::currentNM()->mkNode(APPLY_SELECTOR, s, n);
+}
+
+Node getInstCons(Node n, const DType& dt, size_t index, bool shareSel)
{
Assert(index < dt.getNumConstructors());
std::vector<Node> children;
NodeManager* nm = NodeManager::currentNM();
TypeNode tn = n.getType();
- for (unsigned i = 0, nargs = dt[index].getNumArgs(); i < nargs; i++)
+ for (size_t i = 0, nargs = dt[index].getNumArgs(); i < nargs; i++)
{
Node nc =
- nm->mkNode(APPLY_SELECTOR, dt[index].getSelectorInternal(tn, i), n);
+ nm->mkNode(APPLY_SELECTOR, getSelector(tn, dt[index], i, shareSel), n);
children.push_back(nc);
}
Node n_ic = mkApplyCons(tn, dt, index, children);
Assert(n_ic.getType() == tn);
- Assert(static_cast<size_t>(isInstCons(n, n_ic, dt)) == index);
return n_ic;
}
return nm->mkNode(APPLY_CONSTRUCTOR, cchildren);
}
-int isInstCons(Node t, Node n, const DType& dt)
-{
- if (n.getKind() == APPLY_CONSTRUCTOR)
- {
- int index = indexOf(n.getOperator());
- 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
- || n[i].getOperator() != c.getSelectorInternal(tn, i) || n[i][0] != t)
- {
- return -1;
- }
- }
- return index;
- }
- return -1;
-}
-
int isTester(Node n, Node& a)
{
if (n.getKind() == APPLY_TESTER)
namespace datatypes {
namespace utils {
+/**
+ * Get the index^th selector of datatype constructor dc whose type is dtt. If
+ * shareSel is true, this returns the shared selector of dc.
+ */
+Node getSelector(TypeNode dtt,
+ const DTypeConstructor& dc,
+ size_t index,
+ bool shareSel);
+/**
+ * Apply the indext^th selector of datatype constructor dc to term n. If
+ * shareSel is true, we use the shared selector of dc.
+ */
+Node applySelector(const DTypeConstructor& dc,
+ size_t index,
+ bool shareSel,
+ const Node& n);
+
/** get instantiate cons
*
* 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 DType& dt, size_t index);
+Node getInstCons(Node n, const DType& dt, size_t index, bool shareSel);
/**
* Apply constructor, taking into account whether the datatype is parametric.
*
const DType& dt,
size_t index,
const std::vector<Node>& children);
-/** 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 DType& dt);
/** is tester
*
* This method returns a value >=0 if n is a tester predicate. The return
#include "expr/dtype.h"
#include "expr/dtype_cons.h"
+#include "theory/datatypes/theory_datatypes_utils.h"
using namespace cvc5::internal::kind;
}
TypeNode tn = tuple.getType();
const DType& dt = tn.getDType();
+ // note that shared selectors are irrelevant for datatypes with one
+ // constructor, hence we pass false here
return NodeManager::currentNM()->mkNode(
- APPLY_SELECTOR, dt[0].getSelectorInternal(tn, n_th), tuple);
+ APPLY_SELECTOR, utils::getSelector(tn, dt[0], n_th, false), tuple);
}
Node TupleUtils::getTupleProjection(const std::vector<uint32_t>& indices,
#include "expr/dtype.h"
#include "expr/dtype_cons.h"
#include "expr/node_algorithm.h"
+#include "options/datatypes_options.h"
#include "theory/datatypes/theory_datatypes_utils.h"
using namespace std;
Trace("cegqi-dt-debug") << "try based on constructors in equivalence class."
<< std::endl;
// look in equivalence class for a constructor
- NodeManager* nm = NodeManager::currentNM();
for (unsigned k = 0, size = eqc.size(); k < size; k++)
{
Node n = eqc[k];
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 val = datatypes::utils::getInstCons(
+ pv, dt, cindex, options().datatypes.dtSharedSelectors);
+ for (const Node& c : val)
{
- Node c = nm->mkNode(
- APPLY_SELECTOR, dt[cindex].getSelectorInternal(d_type, j), pv);
ci->pushStackVariable(c);
- children.push_back(c);
}
- Node val = nm->mkNode(kind::APPLY_CONSTRUCTOR, children);
TermProperties pv_prop_dt;
if (ci->constructInstantiationInc(pv, val, pv_prop_dt, sf))
{
}
else
{
- NodeManager* nm = NodeManager::currentNM();
unsigned cindex = DType::indexOf(a.getOperator());
TypeNode tn = a.getType();
const DType& dt = tn.getDType();
- for (unsigned i = 0, nchild = a.getNumChildren(); i < nchild; i++)
+ Node val = datatypes::utils::getInstCons(
+ sb, dt, cindex, options().datatypes.dtSharedSelectors);
+ for (size_t i = 0, nchild = val.getNumChildren(); i < nchild; i++)
{
- Node nn = nm->mkNode(
- APPLY_SELECTOR, dt[cindex].getSelectorInternal(tn, i), sb);
- Node s = solve_dt(v, a[i], Node::null(), sa[i], nn);
+ Node s = solve_dt(v, a[i], Node::null(), sa[i], val[i]);
if (!s.isNull())
{
return s;
#include "expr/dtype.h"
#include "expr/dtype_cons.h"
+#include "options/datatypes_options.h"
#include "options/quantifiers_options.h"
#include "smt/solver_engine.h"
#include "smt/solver_engine_scope.h"
#include "theory/datatypes/datatypes_rewriter.h"
+#include "theory/datatypes/theory_datatypes_utils.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/quantifiers_state.h"
#include "theory/quantifiers/term_database.h"
namespace quantifiers {
namespace inst {
-CandidateGenerator::CandidateGenerator(QuantifiersState& qs, TermRegistry& tr)
- : d_qs(qs), d_treg(tr)
+CandidateGenerator::CandidateGenerator(Env& env,
+ QuantifiersState& qs,
+ TermRegistry& tr)
+ : EnvObj(env), d_qs(qs), d_treg(tr)
{
}
&& !quantifiers::TermUtil::hasInstConstAttr(n);
}
-CandidateGeneratorQE::CandidateGeneratorQE(QuantifiersState& qs,
+CandidateGeneratorQE::CandidateGeneratorQE(Env& env,
+ QuantifiersState& qs,
TermRegistry& tr,
Node pat)
- : CandidateGenerator(qs, tr),
+ : CandidateGenerator(env, qs, tr),
d_termIter(0),
d_termIterList(nullptr),
d_mode(cand_term_none)
return Node::null();
}
-CandidateGeneratorQELitDeq::CandidateGeneratorQELitDeq(QuantifiersState& qs,
+CandidateGeneratorQELitDeq::CandidateGeneratorQELitDeq(Env& env,
+ QuantifiersState& qs,
TermRegistry& tr,
Node mpat)
- : CandidateGenerator(qs, tr), d_match_pattern(mpat)
+ : CandidateGenerator(env, qs, tr), d_match_pattern(mpat)
{
Assert(d_match_pattern.getKind() == EQUAL);
d_match_pattern_type = d_match_pattern[0].getType();
return Node::null();
}
-CandidateGeneratorQEAll::CandidateGeneratorQEAll(QuantifiersState& qs,
+CandidateGeneratorQEAll::CandidateGeneratorQEAll(Env& env,
+ QuantifiersState& qs,
TermRegistry& tr,
Node mpat)
- : CandidateGenerator(qs, tr), d_match_pattern(mpat)
+ : CandidateGenerator(env, qs, tr), d_match_pattern(mpat)
{
d_match_pattern_type = mpat.getType();
Assert(mpat.getKind() == INST_CONSTANT);
{
TNode nh = tdb->getEligibleTermInEqc(n);
if( !nh.isNull() ){
- if (options::instMaxLevel() != -1)
+ if (options().quantifiers.instMaxLevel != -1)
{
nh = d_treg.getModel()->getInternalRepresentative(nh, d_f, d_index);
//don't consider this if already the instantiation is ineligible
return Node::null();
}
-CandidateGeneratorConsExpand::CandidateGeneratorConsExpand(QuantifiersState& qs,
+CandidateGeneratorConsExpand::CandidateGeneratorConsExpand(Env& env,
+ QuantifiersState& qs,
TermRegistry& tr,
Node mpat)
- : CandidateGeneratorQE(qs, tr, mpat)
+ : CandidateGeneratorQE(env, qs, tr, mpat)
{
Assert(mpat.getKind() == APPLY_CONSTRUCTOR);
d_mpat_type = mpat.getType();
{
// generates too many instantiations at top-level when eqc is null, thus
// set mode to none unless option is set.
- if (options::consExpandTriggers())
+ if (options().quantifiers.consExpandTriggers)
{
d_termIterList = d_treg.getTermDatabase()->getGroundTermList(d_op);
d_mode = cand_term_db;
return curr;
}
// expand it
- NodeManager* nm = NodeManager::currentNM();
std::vector<Node> children;
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, dt[0].getSelectorInternal(d_mpat_type, i), curr);
- children.push_back(sel);
- }
- return nm->mkNode(APPLY_CONSTRUCTOR, children);
+ return datatypes::utils::getInstCons(
+ curr, dt, 0, options().datatypes.dtSharedSelectors);
}
bool CandidateGeneratorConsExpand::isLegalOpCandidate(Node n)
return isLegalCandidate(n);
}
-CandidateGeneratorSelector::CandidateGeneratorSelector(QuantifiersState& qs,
+CandidateGeneratorSelector::CandidateGeneratorSelector(Env& env,
+ QuantifiersState& qs,
TermRegistry& tr,
Node mpat)
- : CandidateGeneratorQE(qs, tr, mpat)
+ : CandidateGeneratorQE(env, qs, tr, mpat)
{
Trace("sel-trigger") << "Selector trigger: " << mpat << std::endl;
Assert(mpat.getKind() == APPLY_SELECTOR);
// Get the expanded form of the selector, meaning that we will match on
// the shared selector if shared selectors are enabled.
- Node mpatExp = datatypes::DatatypesRewriter::expandApplySelector(mpat);
+ Node mpatExp = datatypes::DatatypesRewriter::expandApplySelector(
+ mpat, options().datatypes.dtSharedSelectors);
Trace("sel-trigger") << "Expands to: " << mpatExp << std::endl;
Assert (mpatExp.getKind() == APPLY_SELECTOR);
d_selOp = d_treg.getTermDatabase()->getMatchOperator(mpatExp);
#ifndef CVC5__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H
#define CVC5__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H
+#include "smt/env_obj.h"
#include "theory/theory.h"
#include "theory/uf/equality_engine.h"
* }while( !cand.isNull() );
*
*/
-class CandidateGenerator {
+class CandidateGenerator : protected EnvObj
+{
public:
- CandidateGenerator(QuantifiersState& qs, TermRegistry& tr);
+ CandidateGenerator(Env& env, QuantifiersState& qs, TermRegistry& tr);
virtual ~CandidateGenerator(){}
/** reset instantiation round
*
friend class CandidateGeneratorQEDisequal;
public:
- CandidateGeneratorQE(QuantifiersState& qs, TermRegistry& tr, Node pat);
+ CandidateGeneratorQE(Env& env,
+ QuantifiersState& qs,
+ TermRegistry& tr,
+ Node pat);
/** reset */
void reset(Node eqc) override;
/** get next candidate */
* mpat is an equality that we are matching to equalities in the equivalence
* class of false
*/
- CandidateGeneratorQELitDeq(QuantifiersState& qs, TermRegistry& tr, Node mpat);
+ CandidateGeneratorQELitDeq(Env& env,
+ QuantifiersState& qs,
+ TermRegistry& tr,
+ Node mpat);
/** reset */
void reset(Node eqc) override;
/** get next candidate */
std::string identify() const override { return "CandidateGeneratorQEAll"; }
public:
- CandidateGeneratorQEAll(QuantifiersState& qs, TermRegistry& tr, Node mpat);
+ CandidateGeneratorQEAll(Env& env,
+ QuantifiersState& qs,
+ TermRegistry& tr,
+ Node mpat);
/** reset */
void reset(Node eqc) override;
/** get next candidate */
class CandidateGeneratorConsExpand : public CandidateGeneratorQE
{
public:
- CandidateGeneratorConsExpand(QuantifiersState& qs,
+ CandidateGeneratorConsExpand(Env& env,
+ QuantifiersState& qs,
TermRegistry& tr,
Node mpat);
/** reset */
class CandidateGeneratorSelector : public CandidateGeneratorQE
{
public:
- CandidateGeneratorSelector(QuantifiersState& qs, TermRegistry& tr, Node mpat);
+ CandidateGeneratorSelector(Env& env,
+ QuantifiersState& qs,
+ TermRegistry& tr,
+ Node mpat);
/** reset */
void reset(Node eqc) override;
/**
{
// candidates for apply selector are a union of correctly and incorrectly
// applied selectors
- d_cg =
- new inst::CandidateGeneratorSelector(d_qstate, d_treg, d_match_pattern);
+ d_cg = new inst::CandidateGeneratorSelector(
+ d_env, d_qstate, d_treg, d_match_pattern);
}
else if (TriggerTermInfo::isAtomicTriggerKind(mpk))
{
if (dt.getNumConstructors() == 1)
{
d_cg = new inst::CandidateGeneratorConsExpand(
- d_qstate, d_treg, d_match_pattern);
+ d_env, d_qstate, d_treg, d_match_pattern);
}
}
if (d_cg == nullptr)
{
CandidateGeneratorQE* cg =
- new CandidateGeneratorQE(d_qstate, d_treg, d_match_pattern);
+ new CandidateGeneratorQE(d_env, d_qstate, d_treg, d_match_pattern);
// we will be scanning lists trying to find ground terms whose operator
// is the same as d_match_operator's.
d_cg = cg;
Trace("inst-match-gen")
<< "Purify dt trigger " << d_pattern << ", will match terms of op "
<< cOp << std::endl;
- d_cg = new inst::CandidateGeneratorQE(d_qstate, d_treg, cOp);
+ d_cg = new inst::CandidateGeneratorQE(d_env, d_qstate, d_treg, cOp);
}else{
- d_cg = new CandidateGeneratorQEAll(d_qstate, d_treg, d_match_pattern);
+ d_cg =
+ new CandidateGeneratorQEAll(d_env, d_qstate, d_treg, d_match_pattern);
}
}
else if (mpk == EQUAL)
{
// candidates will be all disequalities
d_cg = new inst::CandidateGeneratorQELitDeq(
- d_qstate, d_treg, d_match_pattern);
+ d_env, d_qstate, d_treg, d_match_pattern);
}
}
else
#include "expr/dtype_cons.h"
#include "expr/node_algorithm.h"
#include "expr/skolem_manager.h"
+#include "options/datatypes_options.h"
#include "options/quantifiers_options.h"
#include "theory/arith/arith_msum.h"
#include "theory/datatypes/theory_datatypes_utils.h"
return Node::null();
}
}
- NodeManager* nm = NodeManager::currentNM();
const DType& dt = datatypes::utils::datatypeOf(t.getOperator());
unsigned index = datatypes::utils::indexOf(t.getOperator());
+ bool sharedSel = options().datatypes.dtSharedSelectors;
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 = nm->mkNode(
- APPLY_SELECTOR, dt[index].getSelectorInternal(e.getType(), i), e);
+ Node se = datatypes::utils::applySelector(dt[index], i, sharedSel, e);
u = matchBoundVar( v, t[i], se );
}
if( !u.isNull() ){
NodeManager* nm = NodeManager::currentNM();
for (unsigned j = 0; j < dc.getNumArgs(); j++)
{
- std::vector<Node> ssc;
if (dt.isParametric())
{
Trace("sk-ind-debug") << "Compare " << tspec[j] << " " << ntn
<< std::endl;
- if (tspec[j] == ntn)
+ if (tspec[j] != ntn)
{
- ssc.push_back(n);
+ continue;
}
}
else
{
TypeNode tn = dc[j].getRangeType();
Trace("sk-ind-debug") << "Compare " << tn << " " << ntn << std::endl;
- if (tn == ntn)
+ if (tn != ntn)
{
- ssc.push_back(n);
+ continue;
}
}
- for (unsigned k = 0; k < ssc.size(); k++)
+ // do not use shared selectors
+ Node ss = nm->mkNode(APPLY_SELECTOR, dc.getSelector(j), n);
+ if (std::find(selfSel.begin(), selfSel.end(), ss) == selfSel.end())
{
- Node ss =
- nm->mkNode(APPLY_SELECTOR, dc.getSelectorInternal(n.getType(), j), n);
- if (std::find(selfSel.begin(), selfSel.end(), ss) == selfSel.end())
- {
- selfSel.push_back(ss);
- }
+ selfSel.push_back(ss);
}
}
}
#include "expr/dtype_cons.h"
#include "expr/sygus_datatype.h"
+#include "options/datatypes_options.h"
#include "options/quantifiers_options.h"
#include "theory/datatypes/sygus_datatype_utils.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
}
else
{
+ bool shareSel = options().datatypes.dtSharedSelectors;
Node ret = nm->mkNode(
- APPLY_SELECTOR, dt[i].getSelectorInternal(headType, 0), en[0]);
+ APPLY_SELECTOR,
+ datatypes::utils::getSelector(headType, dt[i], 0, shareSel),
+ en[0]);
Trace("sygus-eval-unfold-debug")
<< "...return (from constructor) " << ret << std::endl;
return ret;
Assert(!dt.isParametric());
std::map<int, Node> pre;
- for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
+ bool sharedSel = options().datatypes.dtSharedSelectors;
+ for (size_t j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
{
std::vector<Node> cc;
Node s;
}
else
{
- s = nm->mkNode(
- APPLY_SELECTOR, dt[i].getSelectorInternal(headType, j), en[0]);
+ Node sel = datatypes::utils::getSelector(headType, dt[i], j, sharedSel);
+ s = nm->mkNode(APPLY_SELECTOR, sel, en[0]);
}
cc.push_back(s);
if (track_exp)
#include "expr/dtype.h"
#include "expr/dtype_cons.h"
+#include "options/datatypes_options.h"
#include "smt/logic_exception.h"
#include "theory/datatypes/sygus_datatype_utils.h"
#include "theory/datatypes/theory_datatypes_utils.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
using namespace cvc5::internal::kind;
-using namespace std;
namespace cvc5::internal {
namespace theory {
return NodeManager::currentNM()->mkNode(d_kind[d], children);
}
+SygusExplain::SygusExplain(Env& env, TermDbSygus* tdb) : EnvObj(env), d_tdb(tdb)
+{
+}
+
void SygusExplain::getExplanationForEquality(Node n,
Node vn,
std::vector<Node>& exp)
int i = datatypes::utils::indexOf(vn.getOperator());
Node tst = datatypes::utils::mkTester(n, i, dt);
exp.push_back(tst);
- for (unsigned j = 0; j < vn.getNumChildren(); j++)
+ bool shareSel = options().datatypes.dtSharedSelectors;
+ for (size_t j = 0, vnc = vn.getNumChildren(); j < vnc; j++)
{
if (cexc.find(j) == cexc.end())
{
- Node sel = NodeManager::currentNM()->mkNode(
- kind::APPLY_SELECTOR, dt[i].getSelectorInternal(tn, j), n);
+ Node sel = datatypes::utils::applySelector(dt[i], j, shareSel, n);
getExplanationForEquality(sel, vn[j], exp);
}
}
vnr_exp = NodeManager::currentNM()->mkConst(true);
}
}
- for (unsigned i = 0; i < vn.getNumChildren(); i++)
+ bool shareSel = options().datatypes.dtSharedSelectors;
+ for (size_t i = 0, vnc = vn.getNumChildren(); i < vnc; i++)
{
- Node sel = NodeManager::currentNM()->mkNode(
- kind::APPLY_SELECTOR, dt[cindex].getSelectorInternal(ntn, i), n);
+ Node sel = datatypes::utils::applySelector(dt[cindex], i, shareSel, n);
Node vnr_c = vnr.isNull() ? vnr : (vn[i] == vnr[i] ? Node::null() : vnr[i]);
if (cexc.find(i) == cexc.end())
{
#include <vector>
#include "expr/node.h"
+#include "smt/env_obj.h"
namespace cvc5::internal {
namespace theory {
* [[exp]]_n = (plus w y)
* where w is a fresh variable.
*/
-class SygusExplain
+class SygusExplain : protected EnvObj
{
public:
- SygusExplain(TermDbSygus* tdb) : d_tdb(tdb) {}
+ SygusExplain(Env& env, TermDbSygus* tdb);
~SygusExplain() {}
/** get explanation for equality
*
TermDbSygus::TermDbSygus(Env& env, QuantifiersState& qs, OracleChecker* oc)
: EnvObj(env),
d_qstate(qs),
- d_syexp(new SygusExplain(this)),
+ d_syexp(new SygusExplain(env, this)),
d_funDefEval(new FunDefEvaluator(env)),
d_eval_unfold(new SygusEvalUnfold(env, this)),
d_ochecker(oc)
SygusTypeInfo& eti = getTypeInfo(et);
std::vector<TypeNode> sf_types;
eti.getSubfieldTypes(sf_types);
+ bool sharedSel = options().datatypes.dtSharedSelectors;
// for each type of subfield type of this enumerator
for (unsigned i = 0, ntypes = sf_types.size(); i < ntypes; i++)
{
// is necessary to generate a term of the form any_constant( x.0 ) for a
// fresh variable x.0.
Node fv = getFreeVar(stn, 0);
- Node exc_val = datatypes::utils::getInstCons(fv, dt, rindex);
+ Node exc_val = datatypes::utils::getInstCons(fv, dt, rindex, sharedSel);
// should not include the constuctor in any subterm
Node x = getFreeVar(stn, 0);
Trace("sygus-db") << "Construct symmetry breaking lemma from " << x
const DType& dt = tn.getDType();
Trace("sygus-db") << "Compute selector weights for " << dt.getName()
<< std::endl;
+ bool sharedSel = options().datatypes.dtSharedSelectors;
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++)
+ for (size_t j = 0, size2 = dt[i].getNumArgs(); j < size2; j++)
{
- Node csel = dt[i].getSelectorInternal(tn, j);
+ Node csel = datatypes::utils::getSelector(tn, dt[i], j, sharedSel);
std::map<Node, unsigned>::iterator its = itsw->second.find(csel);
if (its == itsw->second.end() || cw < its->second)
{
FirstOrderModel* model = d_treg.getModel();
Instantiate* inst = d_qim.getInstantiate();
TermDbSygus* db = d_treg.getTermDatabaseSygus();
- SygusExplain syexplain(db);
+ SygusExplain syexplain(d_env, db);
NodeManager* nm = NodeManager::currentNM();
options::SygusInstMode mode = options().quantifiers.sygusInstMode;
projects / cvc5.git / commitdiff