diff options
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_enumerator.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_eval_unfold.cpp | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_explain.cpp | 10 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_cons.cpp | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_norm.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_pbe.cpp | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_process_conj.cpp | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_repair_const.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif.cpp | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_io.cpp | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_rl.cpp | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_strat.cpp | 7 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.cpp | 17 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/type_info.cpp | 2 |
15 files changed, 24 insertions, 31 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp index bd85ea496..472a82e29 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp @@ -16,7 +16,7 @@ #include "options/datatypes_options.h" #include "options/quantifiers_options.h" -#include "theory/datatypes/datatypes_rewriter.h" +#include "theory/datatypes/theory_datatypes_utils.h" using namespace CVC4::kind; @@ -81,7 +81,7 @@ void SygusEnumerator::initialize(Node e) if (sbl.getKind() == NOT) { Node a; - int tst = datatypes::DatatypesRewriter::isTester(sbl[0], a); + int tst = datatypes::utils::isTester(sbl[0], a); if (tst >= 0) { if (a == e) diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp index 7324add50..5286ab6f7 100644 --- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp @@ -15,7 +15,6 @@ #include "theory/quantifiers/sygus/sygus_eval_unfold.h" #include "options/quantifiers_options.h" -#include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/sygus/term_database_sygus.h" using namespace std; diff --git a/src/theory/quantifiers/sygus/sygus_explain.cpp b/src/theory/quantifiers/sygus/sygus_explain.cpp index f55ce2097..b1baed9cb 100644 --- a/src/theory/quantifiers/sygus/sygus_explain.cpp +++ b/src/theory/quantifiers/sygus/sygus_explain.cpp @@ -14,7 +14,7 @@ #include "theory/quantifiers/sygus/sygus_explain.h" -#include "theory/datatypes/datatypes_rewriter.h" +#include "theory/datatypes/theory_datatypes_utils.h" #include "theory/quantifiers/sygus/term_database_sygus.h" using namespace CVC4::kind; @@ -139,8 +139,8 @@ void SygusExplain::getExplanationForEquality(Node n, } Assert(vn.getKind() == kind::APPLY_CONSTRUCTOR); const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype(); - int i = datatypes::DatatypesRewriter::indexOf(vn.getOperator()); - Node tst = datatypes::DatatypesRewriter::mkTester(n, i, dt); + 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++) { @@ -223,9 +223,9 @@ void SygusExplain::getExplanationFor(TermRecBuild& trb, } } const Datatype& dt = ((DatatypeType)ntn.toType()).getDatatype(); - int cindex = datatypes::DatatypesRewriter::indexOf(vn.getOperator()); + int cindex = datatypes::utils::indexOf(vn.getOperator()); Assert(cindex >= 0 && cindex < (int)dt.getNumConstructors()); - Node tst = datatypes::DatatypesRewriter::mkTester(n, cindex, dt); + Node tst = datatypes::utils::mkTester(n, cindex, dt); exp.push_back(tst); // if the operator of vn is different than vnr, then disunification obligation // is met diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 43696bff0..0dc49fa96 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -20,7 +20,6 @@ #include "options/quantifiers_options.h" #include "printer/sygus_print_callback.h" #include "theory/bv/theory_bv_utils.h" -#include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/sygus/sygus_grammar_norm.h" #include "theory/quantifiers/sygus/sygus_process_conj.h" #include "theory/quantifiers/sygus/synth_conjecture.h" diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp index ebb92b34b..5e8c9c411 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp @@ -20,7 +20,7 @@ #include "printer/sygus_print_callback.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" -#include "theory/datatypes/datatypes_rewriter.h" +#include "theory/datatypes/theory_datatypes_utils.h" #include "theory/quantifiers/cegqi/ceg_instantiator.h" #include "theory/quantifiers/sygus/sygus_grammar_red.h" #include "theory/quantifiers/sygus/term_database_sygus.h" diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index c76082b02..64bf0972c 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -16,7 +16,6 @@ #include "expr/datatype.h" #include "options/quantifiers_options.h" -#include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.cpp b/src/theory/quantifiers/sygus/sygus_process_conj.cpp index 2b9592d4d..66e80523a 100644 --- a/src/theory/quantifiers/sygus/sygus_process_conj.cpp +++ b/src/theory/quantifiers/sygus/sygus_process_conj.cpp @@ -18,7 +18,6 @@ #include "expr/datatype.h" #include "options/quantifiers_options.h" -#include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index 39506b593..5511adb18 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -20,7 +20,7 @@ #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" -#include "theory/datatypes/datatypes_rewriter.h" +#include "theory/datatypes/theory_datatypes_utils.h" #include "theory/quantifiers/cegqi/ceg_instantiator.h" #include "theory/quantifiers/sygus/sygus_grammar_norm.h" #include "theory/quantifiers/sygus/term_database_sygus.h" @@ -372,7 +372,7 @@ bool SygusRepairConst::isRepairable(Node n, bool useConstantsAsHoles) return false; } Node op = n.getOperator(); - unsigned cindex = datatypes::DatatypesRewriter::indexOf(op); + unsigned cindex = datatypes::utils::indexOf(op); Node sygusOp = Node::fromExpr(dt[cindex].getSygusOp()); if (sygusOp.getAttribute(SygusAnyConstAttribute())) { diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp index 008947adb..fdc8120ff 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif.cpp @@ -14,7 +14,6 @@ #include "theory/quantifiers/sygus/sygus_unif.h" -#include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index 207aa4c8e..ff58dbe38 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -15,7 +15,6 @@ #include "theory/quantifiers/sygus/sygus_unif_io.h" #include "options/quantifiers_options.h" -#include "theory/datatypes/datatypes_rewriter.h" #include "theory/evaluator.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index 3514ccbeb..3f09a4346 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -17,7 +17,6 @@ #include "options/base_options.h" #include "options/quantifiers_options.h" #include "printer/printer.h" -#include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "util/random.h" diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp index a41d895b3..e74068ace 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp @@ -14,7 +14,7 @@ #include "theory/quantifiers/sygus/sygus_unif_strat.h" -#include "theory/datatypes/datatypes_rewriter.h" +#include "theory/datatypes/theory_datatypes_utils.h" #include "theory/quantifiers/sygus/sygus_unif.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" @@ -735,8 +735,7 @@ void SygusUnifStrategy::staticLearnRedundantOps( Assert(nc.first < dt.getNumConstructors()); if (!nc.second) { - Node tst = - datatypes::DatatypesRewriter::mkTester(em, nc.first, dt).negate(); + Node tst = datatypes::utils::mkTester(em, nc.first, dt).negate(); if (std::find(lemmas.begin(), lemmas.end(), tst) == lemmas.end()) { @@ -802,7 +801,7 @@ void SygusUnifStrategy::staticLearnRedundantOps( continue; } EnumTypeInfoStrat* etis = snode.d_strats[j]; - unsigned cindex = datatypes::DatatypesRewriter::indexOf(etis->d_cons); + unsigned cindex = datatypes::utils::indexOf(etis->d_cons); // constructors that correspond to strategies are not needed // the intuition is that the strategy itself is responsible for constructing // all terms that use the given constructor diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index e2a8540d4..78f2f6a7e 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -23,7 +23,7 @@ #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" -#include "theory/datatypes/datatypes_rewriter.h" +#include "theory/datatypes/theory_datatypes_utils.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quantifiers_attributes.h" diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index ed3eec145..ff9fede0b 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -16,10 +16,11 @@ #include "base/cvc4_check.h" #include "options/base_options.h" +#include "options/datatypes_options.h" #include "options/quantifiers_options.h" #include "printer/printer.h" #include "theory/arith/arith_msum.h" -#include "theory/datatypes/datatypes_rewriter.h" +#include "theory/datatypes/theory_datatypes_utils.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" @@ -184,7 +185,7 @@ Node TermDbSygus::mkGeneric(const Datatype& dt, Assert( !a.isNull() ); children.push_back( a ); } - return datatypes::DatatypesRewriter::mkSygusTerm(dt, c, children); + return datatypes::utils::mkSygusTerm(dt, c, children); } Node TermDbSygus::mkGeneric(const Datatype& dt, int c, std::map<int, Node>& pre) @@ -286,7 +287,7 @@ Node TermDbSygus::sygusToBuiltin(Node n, TypeNode tn) } if (n.getKind() == APPLY_CONSTRUCTOR) { - unsigned i = datatypes::DatatypesRewriter::indexOf(n.getOperator()); + unsigned i = datatypes::utils::indexOf(n.getOperator()); Assert(n.getNumChildren() == dt[i].getNumArgs()); std::map<int, Node> pre; for (unsigned j = 0, size = n.getNumChildren(); j < size; j++) @@ -325,7 +326,7 @@ unsigned TermDbSygus::getSygusTermSize( Node n ){ sum += getSygusTermSize(n[i]); } const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr()); - int cindex = datatypes::DatatypesRewriter::indexOf(n.getOperator()); + int cindex = datatypes::utils::indexOf(n.getOperator()); Assert(cindex >= 0 && cindex < (int)dt.getNumConstructors()); unsigned weight = dt[cindex].getWeight(); return weight + sum; @@ -422,7 +423,7 @@ void TermDbSygus::registerEnumerator(Node e, // 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::DatatypesRewriter::getInstCons(fv, dt, rindex); + Node exc_val = datatypes::utils::getInstCons(fv, dt, rindex); // should not include the constuctor in any subterm Node x = getFreeVar(stn, 0); Trace("sygus-db") << "Construct symmetry breaking lemma from " << x @@ -776,7 +777,7 @@ bool TermDbSygus::isSymbolicConsApp(Node n) const Assert(tn.isDatatype()); const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype(); Assert(dt.isSygus()); - unsigned cindex = datatypes::DatatypesRewriter::indexOf(n.getOperator()); + unsigned cindex = datatypes::utils::indexOf(n.getOperator()); Node sygusOp = Node::fromExpr(dt[cindex].getSygusOp()); // it is symbolic if it represents "any constant" return sygusOp.getAttribute(SygusAnyConstAttribute()); @@ -948,7 +949,7 @@ Node TermDbSygus::unfold( Node en, std::map< Node, Node >& vtm, std::vector< Nod Type headType = en[0].getType().toType(); NodeManager* nm = NodeManager::currentNM(); const Datatype& dt = static_cast<DatatypeType>(headType).getDatatype(); - unsigned i = datatypes::DatatypesRewriter::indexOf(ev.getOperator()); + unsigned i = datatypes::utils::indexOf(ev.getOperator()); if (track_exp) { // explanation @@ -1007,7 +1008,7 @@ Node TermDbSygus::unfold( Node en, std::map< Node, Node >& vtm, std::vector< Nod } Node ret = mkGeneric(dt, i, pre); // apply the appropriate substitution to ret - ret = datatypes::DatatypesRewriter::applySygusArgs(dt, sop, ret, args); + ret = datatypes::utils::applySygusArgs(dt, sop, ret, args); // rewrite ret = Rewriter::rewrite(ret); return ret; diff --git a/src/theory/quantifiers/sygus/type_info.cpp b/src/theory/quantifiers/sygus/type_info.cpp index 070e2ad9a..818a53711 100644 --- a/src/theory/quantifiers/sygus/type_info.cpp +++ b/src/theory/quantifiers/sygus/type_info.cpp @@ -15,7 +15,7 @@ #include "theory/quantifiers/sygus/type_info.h" #include "base/cvc4_check.h" -#include "theory/datatypes/datatypes_rewriter.h" +#include "theory/datatypes/theory_datatypes_utils.h" #include "theory/quantifiers/sygus/term_database_sygus.h" using namespace CVC4::kind; |