diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-11-18 13:52:18 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-11-18 13:52:18 -0600 |
commit | 6fe7877d82721e453d5d928a8fe9dbad2099dac1 (patch) | |
tree | 3e4c6ef5d0b802db5f76d7cbac66a792f28c6dc7 /src/theory | |
parent | 357e81dfc393d9e2ea80f66cddc837564494a34c (diff) |
Use standard sygus interface for abduction and rewrite rule synthesis (#3471)
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_abduct.cpp | 29 |
1 files changed, 17 insertions, 12 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp index 529ef037f..0396aba86 100644 --- a/src/theory/quantifiers/sygus/sygus_abduct.cpp +++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp @@ -17,6 +17,7 @@ #include "expr/datatype.h" #include "expr/node_algorithm.h" +#include "expr/sygus_datatype.h" #include "printer/sygus_print_callback.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_rewriter.h" @@ -86,7 +87,7 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name, { Assert(abdGType.isDatatype() && abdGType.getDatatype().isSygus()); // must convert all constructors to version with bound variables in "vars" - std::vector<Datatype> datatypes; + std::vector<SygusDatatype> sdts; std::set<Type> unres; Trace("sygus-abduct-debug") << "Process abduction type:" << std::endl; @@ -129,9 +130,9 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name, const Datatype& dtc = curr.getDatatype(); std::stringstream ssdtn; ssdtn << dtc.getName() << "_s"; - datatypes.push_back(Datatype(ssdtn.str())); + sdts.push_back(SygusDatatype(ssdtn.str())); Trace("sygus-abduct-debug") - << "Process datatype " << datatypes.back().getName() << "..." + << "Process datatype " << sdts.back().getName() << "..." << std::endl; for (unsigned j = 0, ncons = dtc.getNumConstructors(); j < ncons; j++) { @@ -141,7 +142,7 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name, syms.begin(), syms.end(), varlist.begin(), varlist.end()); Trace("sygus-abduct-debug") << " Process constructor " << op << " / " << ops << "..." << std::endl; - std::vector<Type> cargs; + std::vector<TypeNode> cargs; for (unsigned k = 0, nargs = dtc[j].getNumArgs(); k < nargs; k++) { TypeNode argt = TypeNode::fromType(dtc[j].getArgType(k)); @@ -167,7 +168,7 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name, } Trace("sygus-abduct-debug") << " Arg #" << k << ": " << argtNew << std::endl; - cargs.push_back(argtNew.toType()); + cargs.push_back(argtNew); } // callback prints as the expression std::shared_ptr<SygusPrintCallback> spc; @@ -191,22 +192,26 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name, ss << ops.getKind(); Trace("sygus-abduct-debug") << "Add constructor : " << ops << std::endl; - datatypes.back().addSygusConstructor( - ops.toExpr(), ss.str(), cargs, spc); + sdts.back().addConstructor(ops, ss.str(), cargs, spc); } Trace("sygus-abduct-debug") << "Set sygus : " << dtc.getSygusType() << " " << abvl << std::endl; - datatypes.back().setSygus(dtc.getSygusType(), - abvl.toExpr(), - dtc.getSygusAllowConst(), - dtc.getSygusAllowAll()); + TypeNode stn = TypeNode::fromType(dtc.getSygusType()); + sdts.back().initializeDatatype( + stn, abvl, dtc.getSygusAllowConst(), dtc.getSygusAllowAll()); } dtToProcess.clear(); dtToProcess.insert( dtToProcess.end(), dtNextToProcess.begin(), dtNextToProcess.end()); } Trace("sygus-abduct-debug") - << "Make " << datatypes.size() << " datatype types..." << std::endl; + << "Make " << sdts.size() << " datatype types..." << std::endl; + // extract the datatypes + std::vector<Datatype> datatypes; + for (unsigned i = 0, ndts = sdts.size(); i < ndts; i++) + { + datatypes.push_back(sdts[i].getDatatype()); + } // make the datatype types std::vector<DatatypeType> datatypeTypes = nm->toExprManager()->mkMutualDatatypeTypes( |