From e63544462eb850a27f7b416f2f0613efb96eef1d Mon Sep 17 00:00:00 2001 From: Ying Sheng Date: Tue, 28 Jul 2020 09:55:52 -0700 Subject: [PATCH] Interpolation: Add interface for SyGuS interpolation module (step3) (#4726) This is the 3rd step of adding interface for SyGuS Interpolation module. The whole change will be adding the API for (get-interpol s B), which is aim for computes an I that A->I and I->B. Here A is the assertions in the stack. The 3rd step partially implemented the interpolation module. --- .../quantifiers/sygus/sygus_interpol.cpp | 145 +++++++++++++++++- src/theory/quantifiers/sygus/sygus_interpol.h | 46 ++++-- 2 files changed, 170 insertions(+), 21 deletions(-) diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp index 42572a0c7..31f975786 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.cpp +++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp @@ -39,25 +39,160 @@ SygusInterpol::SygusInterpol(LogicInfo logic) : d_logic(logic) {} void SygusInterpol::collectSymbols(const std::vector& axioms, const Node& conj) { + Trace("sygus-interpol-debug") << "Collect symbols..." << std::endl; + std::unordered_set symSetAxioms; + std::unordered_set symSetConj; + for (size_t i = 0, size = axioms.size(); i < size; i++) + { + expr::getSymbols(axioms[i], symSetAxioms); + } + expr::getSymbols(conj, symSetConj); + d_syms.insert(d_syms.end(), symSetAxioms.begin(), symSetAxioms.end()); + d_syms.insert(d_syms.end(), symSetConj.begin(), symSetConj.end()); + for (const Node& elem : symSetConj) + { + if (symSetAxioms.find(elem) != symSetAxioms.end()) + { + d_symSetShared.insert(elem); + } + } + Trace("sygus-interpol-debug") + << "...finish, got " << d_syms.size() << " symbols in total. And " + << d_symSetShared.size() << " shared symbols." << std::endl; } void SygusInterpol::createVariables(bool needsShared) { + NodeManager* nm = NodeManager::currentNM(); + for (const Node& s : d_syms) + { + TypeNode tn = s.getType(); + if (tn.isConstructor() || tn.isSelector() || tn.isTester()) + { + // datatype symbols should be considered interpreted symbols here, not + // (higher-order) variables. + continue; + } + // Notice that we allow for non-first class (e.g. function) variables here. + std::stringstream ss; + ss << s; + Node var = nm->mkBoundVar(tn); + d_vars.push_back(var); + Node vlv = nm->mkBoundVar(ss.str(), tn); + d_vlvs.push_back(vlv); + if (!needsShared || d_symSetShared.find(s) != d_symSetShared.end()) + { + d_varsShared.push_back(var); + d_vlvsShared.push_back(vlv); + d_varTypesShared.push_back(tn); + } + } + // make the sygus variable list + d_ibvlShared = nm->mkNode(kind::BOUND_VAR_LIST, d_vlvsShared); + Trace("sygus-interpol-debug") << "...finish" << std::endl; } -std::map > getIncludeCons( - const std::vector& assumptions, const Node& conclusion) +void SygusInterpol::getIncludeCons( + const std::vector& axioms, + const Node& conj, + std::map>& result) { - std::map > result = - std::map >(); - return result; + NodeManager* nm = NodeManager::currentNM(); + Assert(options::produceInterpols() != options::ProduceInterpols::NONE); + // ASSUMPTIONS + if (options::produceInterpols() == options::ProduceInterpols::ASSUMPTIONS) + { + Node tmpAssumptions = + (axioms.size() == 1 ? axioms[0] : nm->mkNode(kind::AND, axioms)); + expr::getOperatorsMap(tmpAssumptions, result); + } + // CONJECTURE + else if (options::produceInterpols() == options::ProduceInterpols::CONJECTURE) + { + expr::getOperatorsMap(conj, result); + } + // SHARED + else if (options::produceInterpols() == options::ProduceInterpols::SHARED) + { + // Get operators from axioms + std::map> + include_cons_axioms; + Node tmpAssumptions = + (axioms.size() == 1 ? axioms[0] : nm->mkNode(kind::AND, axioms)); + expr::getOperatorsMap(tmpAssumptions, include_cons_axioms); + + // Get operators from conj + std::map> + include_cons_conj; + expr::getOperatorsMap(conj, include_cons_conj); + + // Compute intersection + for (auto& [tn, axiomsOps] : include_cons_axioms) + { + std::map>::iterator + concIter = include_cons_conj.find(tn); + if (concIter != include_cons_conj.end()) + { + std::unordered_set conjOps = concIter->second; + for (const Node& n : axiomsOps) + { + if (conjOps.find(n) != conjOps.end()) + { + if (result.find(tn) == result.end()) + { + result[tn] = std::unordered_set(); + } + result[tn].insert(n); + } + } + } + } + } + // ALL + else if (options::produceInterpols() == options::ProduceInterpols::ALL) + { + Node tmpAssumptions = + (axioms.size() == 1 ? axioms[0] : nm->mkNode(kind::AND, axioms)); + Node tmpAll = nm->mkNode(kind::AND, tmpAssumptions, conj); + expr::getOperatorsMap(tmpAll, result); + } } TypeNode SygusInterpol::setSynthGrammar(const TypeNode& itpGType, const std::vector& axioms, const Node& conj) { + Trace("sygus-interpol-debug") << "Setup grammar..." << std::endl; TypeNode itpGTypeS; + if (!itpGType.isNull()) + { + // set user-defined grammar + Assert(itpGType.isDatatype() && itpGType.getDType().isSygus()); + itpGTypeS = datatypes::utils::substituteAndGeneralizeSygusType( + itpGType, d_syms, d_vlvs); + Assert(itpGTypeS.isDatatype() && itpGTypeS.getDType().isSygus()); + // TODO(Ying Sheng) check if the vars in user-defined grammar, are + // consistent with the shared vars + } + else + { + // set default grammar + std::map> extra_cons; + std::map> exclude_cons; + std::map> include_cons; + getIncludeCons(axioms, conj, include_cons); + std::unordered_set terms_irrelevant; + itpGTypeS = + CVC4::theory::quantifiers::CegGrammarConstructor::mkSygusDefaultType( + NodeManager::currentNM()->booleanType(), + d_ibvlShared, + "interpolation_grammar", + extra_cons, + exclude_cons, + include_cons, + terms_irrelevant); + } + Trace("sygus-interpol-debug") << "...finish setting up grammar" << std::endl; return itpGTypeS; } diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h index 4655822ec..a79d583cd 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.h +++ b/src/theory/quantifiers/sygus/sygus_interpol.h @@ -71,7 +71,7 @@ class SygusInterpol /** * Collects symbols from axioms (axioms) and conjecture (conj), which are * stored in d_syms, and computes the shared symbols between axioms and - * conjecture, stored in d_symsShared. + * conjecture, stored in d_symSetShared. * * @param axioms the assertions (Fa above) * @param conj the conjecture (Fc above) @@ -80,11 +80,11 @@ class SygusInterpol /** * Creates free variables and shared free variables from d_syms and - * d_symsShared, which are stored in d_vars and d_varsShared. And also creates - * the corresponding set of variables for the formal argument list, which is - * stored in d_vlvs and d_vlvsShared. Extracts the types of shared variables, - * which are stored in d_varTypesShared. Creates the formal argument list of - * the interpol-to-synthesis, stored in d_ibvlShared. + * d_symSetShared, which are stored in d_vars and d_varsShared. And also + * creates the corresponding set of variables for the formal argument list, + * which is stored in d_vlvs and d_vlvsShared. Extracts the types of shared + * variables, which are stored in d_varTypesShared. Creates the formal + * argument list of the interpol-to-synthese, stored in d_ibvlShared. * * When using default grammar, the needsShared is true. When using * user-defined gramar, the needsShared is false. @@ -95,18 +95,33 @@ class SygusInterpol */ void createVariables(bool needsShared); + /** + * Get include_cons for mkSygusDefaultType. + * mkSygusDefaultType() is a function to make default grammar. It has an + * arguemnt include_cons, which will restrict what operators we want in the + * grammar. The return value depends on options::produceInterpols(). In + * ASSUMPTIONS option, it will return the operators from axioms. In CONJECTURE + * option, it will return the operators from conj. In SHARED option, it will + * return the oprators shared by axioms and conj. In ALL option, it will + * return the operators from either axioms or conj. + * + * @param axioms input argument + * @param conj input argument + * @param result the return value + */ + void getIncludeCons( + const std::vector& axioms, + const Node& conj, + std::map>& result); + /** * Set up the grammar for the interpol-to-synthesis. * * The user-defined grammar will be encoded by itpGType. The options for * grammar is given by options::produceInterpols(). In DEFAULT option, it will * set up the grammar from itpGType. And if itpGType is null, it will set up - * the default grammar. In ASSUMPTIONS option, it will set up the grammar by - * only using the operators from axioms. In CONJECTURE option, it will set up - * the grammar by only using the operators from conj. In SHARED option, it - * will set up the grammar by only using the operators shared by axioms and - * conj. In ALL option, it will set up the grammar by only using the operators - * from either axioms or conj. + * the default grammar, which is built according to a policy handled by + * getIncludeCons(). * * @param itpGType (if non-null) a sygus datatype type that encodes the * grammar that should be used for solutions of the interpolation conjecture. @@ -165,15 +180,14 @@ class SygusInterpol * The logic for the local copy of SMT engine (d_subSolver). */ LogicInfo d_logic; - /** * symbols from axioms and conjecture. */ std::vector d_syms; /** - * shared symbols between axioms and conjecture. + * unordered set for shared symbols between axioms and conjecture. */ - std::vector d_symsShared; + std::unordered_set d_symSetShared; /** * free variables created from d_syms. */ @@ -183,7 +197,7 @@ class SygusInterpol */ std::vector d_vlvs; /** - * free variables created from d_symsShared. + * free variables created from d_symSetShared. */ std::vector d_varsShared; /** -- 2.30.2