void SygusInterpol::collectSymbols(const std::vector<Node>& axioms,
const Node& conj)
{
+ Trace("sygus-interpol-debug") << "Collect symbols..." << std::endl;
+ std::unordered_set<Node, NodeHashFunction> symSetAxioms;
+ std::unordered_set<Node, NodeHashFunction> 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<TypeNode, std::unordered_set<Node, NodeHashFunction> > getIncludeCons(
- const std::vector<Node>& assumptions, const Node& conclusion)
+void SygusInterpol::getIncludeCons(
+ const std::vector<Node>& axioms,
+ const Node& conj,
+ std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& result)
{
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction> > result =
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction> >();
- 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<TypeNode, std::unordered_set<Node, NodeHashFunction>>
+ 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<TypeNode, std::unordered_set<Node, NodeHashFunction>>
+ include_cons_conj;
+ expr::getOperatorsMap(conj, include_cons_conj);
+
+ // Compute intersection
+ for (auto& [tn, axiomsOps] : include_cons_axioms)
+ {
+ std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>::iterator
+ concIter = include_cons_conj.find(tn);
+ if (concIter != include_cons_conj.end())
+ {
+ std::unordered_set<Node, NodeHashFunction> 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<Node, NodeHashFunction>();
+ }
+ 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<Node>& 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<TypeNode, std::unordered_set<Node, NodeHashFunction>> extra_cons;
+ std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> exclude_cons;
+ std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> include_cons;
+ getIncludeCons(axioms, conj, include_cons);
+ std::unordered_set<Node, NodeHashFunction> 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;
}
/**
* 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)
/**
* 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.
*/
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<Node>& axioms,
+ const Node& conj,
+ std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& 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.
* The logic for the local copy of SMT engine (d_subSolver).
*/
LogicInfo d_logic;
-
/**
* symbols from axioms and conjecture.
*/
std::vector<Node> d_syms;
/**
- * shared symbols between axioms and conjecture.
+ * unordered set for shared symbols between axioms and conjecture.
*/
- std::vector<Node> d_symsShared;
+ std::unordered_set<Node, NodeHashFunction> d_symSetShared;
/**
* free variables created from d_syms.
*/
*/
std::vector<Node> d_vlvs;
/**
- * free variables created from d_symsShared.
+ * free variables created from d_symSetShared.
*/
std::vector<Node> d_varsShared;
/**
projects / cvc5.git / commitdiff