theory/quantifiers/sygus/sygus_module.h \
theory/quantifiers/sygus/sygus_process_conj.cpp \
theory/quantifiers/sygus/sygus_process_conj.h \
+ theory/quantifiers/sygus/sygus_repair_const.cpp \
+ theory/quantifiers/sygus/sygus_repair_const.h \
theory/quantifiers/sygus/sygus_unif.cpp \
theory/quantifiers/sygus/sygus_unif.h \
theory/quantifiers/sygus/sygus_unif_io.cpp \
read_only = true
help = "use quantifier elimination as a preprocessing step for sygus"
+[[option]]
+ name = "sygusRepairConst"
+ category = "regular"
+ long = "sygus-repair-const"
+ type = "bool"
+ default = "false"
+ help = "use approach to repair constants in sygus candidate solutions"
+
[[option]]
name = "sygusMinGrammar"
category = "regular"
options::cbqiMidpoint.set(true);
}
}
+ else
+ {
+ // cannot use sygus repair constants
+ options::sygusRepairConst.set(false);
+ }
if(options::forceLogicString.wasSetByUser()) {
d_logic = LogicInfo(options::forceLogicString());
// cases where we need produce models
if (!options::produceModels()
- && (options::produceAssignments() || options::sygusRewSynthCheck()))
+ && (options::produceAssignments() || options::sygusRewSynthCheck()
+ || options::sygusRepairConst()))
{
Notice() << "SmtEngine: turning on produce-models" << endl;
setOption("produce-models", SExpr("true"));
map<Node, Node> sol_map;
/* Get solutions and build auxiliary vectors for substituting */
d_theoryEngine->getSynthSolutions(sol_map);
+ if (sol_map.empty())
+ {
+ Trace("check-synth-sol") << "No solution to check!\n";
+ return;
+ }
Trace("check-synth-sol") << "Got solution map:\n";
std::vector<Node> function_vars, function_sols;
for (const auto& pair : sol_map)
else if (r.asSatisfiabilityResult().isSat())
{
InternalError(
- "SmtEngine::checkSynhtSol(): produced solution allows satisfiable "
- "negated conjecture.");
+ "SmtEngine::checkSynthSolution(): produced solution leads to "
+ "satisfiable negated conjecture.");
}
solChecker.resetAssertions();
}
Trace("sygus-sb") << " SygusSymBreakNew::check: finished." << std::endl;
if( Trace.isOn("cegqi-engine") ){
- if( lemmas.empty() ){
+ if (lemmas.empty() && !d_szinfo.empty())
+ {
Trace("cegqi-engine") << "*** Sygus : passed datatypes check. term size(s) : ";
for( std::map< Node, SearchSizeInfo * >::iterator it = d_szinfo.begin(); it != d_szinfo.end(); ++it ){
SearchSizeInfo * s = it->second;
if (lit[1].getType() == lit.getType())
{
// t != s ---> ~t = s
- Assert(lit[1].getKind() != notk);
- eq = nm->mkNode(EQUAL, TermUtil::mkNegate(notk, lit[0]), lit[1]);
+ if (lit[1].getKind() == notk && lit[0].getKind() != notk)
+ {
+ eq = nm->mkNode(EQUAL, lit[0], TermUtil::mkNegate(notk, lit[1]));
+ }
+ else
+ {
+ eq = nm->mkNode(EQUAL, TermUtil::mkNegate(notk, lit[0]), lit[1]);
+ }
}
}
else
{
n = slv_eq;
}
- NodeManager* nm = NodeManager::currentNM();
-
Node v[2];
for (unsigned i = 0; i < 2; i++)
{
d_ceg_si(new CegConjectureSingleInv(qe, this)),
d_ceg_proc(new CegConjectureProcess(qe)),
d_ceg_gc(new CegGrammarConstructor(qe, this)),
+ d_sygus_rconst(new SygusRepairConst(qe)),
d_ceg_pbe(new CegConjecturePbe(qe, this)),
d_ceg_cegis(new Cegis(qe, this)),
d_ceg_cegisUnif(new CegisUnif(qe, this)),
d_master(nullptr),
+ d_repair_index(0),
d_refine_count(0),
d_syntax_guided(false)
{
d_embed_quant, vars, d_candidates));
Trace("cegqi") << "Base instantiation is : " << d_base_inst << std::endl;
+ // initialize the sygus constant repair utility
+ if (options::sygusRepairConst())
+ {
+ d_sygus_rconst->initialize(d_base_inst, d_candidates);
+ }
+
// register this term with sygus database and other utilities that impact
// the enumerative sygus search
std::vector< Node > guarded_lemmas;
std::vector<Node> terms;
d_master->getTermList(d_candidates, terms);
- // get their model value
+ Assert(!d_candidates.empty());
+
+ Trace("cegqi-check") << "CegConjuncture : check, build candidates..."
+ << std::endl;
+ std::vector<Node> candidate_values;
+ bool constructed_cand = false;
+
+ if (options::sygusRepairConst())
+ {
+ // have we tried to repair the previous solution?
+ // if not, call the repair constant utility
+ unsigned ninst = d_cinfo[d_candidates[0]].d_inst.size();
+ if (d_repair_index < ninst)
+ {
+ std::vector<Node> fail_cvs;
+ for (const Node& cprog : d_candidates)
+ {
+ Assert(d_repair_index < d_cinfo[cprog].d_inst.size());
+ fail_cvs.push_back(d_cinfo[cprog].d_inst[d_repair_index]);
+ }
+ d_repair_index++;
+ if (d_sygus_rconst->repairSolution(
+ d_candidates, fail_cvs, candidate_values))
+ {
+ constructed_cand = true;
+ }
+ }
+ }
+
+ // get the model value of the relevant terms from the master module
std::vector<Node> enum_values;
getModelValues(terms, enum_values);
- std::vector<Node> candidate_values;
- Trace("cegqi-check") << "CegConjuncture : check, build candidates..." << std::endl;
- bool constructed_cand = d_master->constructCandidates(
- terms, enum_values, d_candidates, candidate_values, lems);
+ if (!constructed_cand)
+ {
+ Assert(candidate_values.empty());
+ constructed_cand = d_master->constructCandidates(
+ terms, enum_values, d_candidates, candidate_values, lems);
+ }
NodeManager* nm = NodeManager::currentNM();
#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
#include "theory/quantifiers/sygus/sygus_pbe.h"
#include "theory/quantifiers/sygus/sygus_process_conj.h"
+#include "theory/quantifiers/sygus/sygus_repair_const.h"
+#include "theory/quantifiers/sygus_sampler.h"
#include "theory/quantifiers_engine.h"
namespace CVC4 {
/** get model value for term n */
Node getModelValue( Node n );
- /** get program by examples utility */
- CegConjecturePbe* getPbe() { return d_ceg_pbe.get(); }
/** get utility for static preprocessing and analysis of conjectures */
CegConjectureProcess* getProcess() { return d_ceg_proc.get(); }
+ /** get constant repair utility */
+ SygusRepairConst* getRepairConst() { return d_sygus_rconst.get(); }
+ /** get program by examples module */
+ CegConjecturePbe* getPbe() { return d_ceg_pbe.get(); }
/** get the symmetry breaking predicate for type */
Node getSymmetryBreakingPredicate(
Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth);
std::unique_ptr<CegConjectureProcess> d_ceg_proc;
/** grammar utility */
std::unique_ptr<CegGrammarConstructor> d_ceg_gc;
+ /** repair constant utility */
+ std::unique_ptr<SygusRepairConst> d_sygus_rconst;
//------------------------modules
/** program by examples module */
std::vector< Node > d_candidates;
/** base instantiation
* If d_embed_quant is forall d. exists y. P( d, y ), then
- * this is the formula exists y. P( d_candidates, y ).
+ * this is the formula exists y. P( d_candidates, y ). Notice that
+ * (exists y. F) is shorthand above for ~( forall y. ~F ).
*/
Node d_base_inst;
/** list of variables on inner quantification */
/** list of terms we have instantiated candidates with */
std::vector< Node > d_inst;
};
- std::map< Node, CandidateInfo > d_cinfo;
+ std::map<Node, CandidateInfo> d_cinfo;
+ /**
+ * The first index of an instantiation in CandidateInfo::d_inst that we have
+ * not yet tried to repair.
+ */
+ unsigned d_repair_index;
/** number of times we have called doRefine */
unsigned d_refine_count;
/** get candidadate */
{
d_conj->getSynthSolutions(sol_map, d_last_inst_si);
}
- else
- {
- Assert(false);
- }
}
void CegInstantiation::preregisterAssertion( Node n ) {
// them, return a proxy
if (!options::cegqiSingleInvReconstructConst() || dt.getSygusAllowConst())
{
- Node k = nm->mkSkolem("sy", tn, "sygus proxy");
- SygusPrintProxyAttribute spa;
- k.setAttribute(spa, c);
- sc = k;
+ sc = tds->getProxyVariable(tn, c);
}
else
{
{
if (addEvalLemmas(enums, enum_values))
{
+ // it may be repairable
+ SygusRepairConst* src = d_parent->getRepairConst();
+ std::vector<Node> fail_cvs = enum_values;
+ if (src->repairSolution(candidates, fail_cvs, candidate_values))
+ {
+ return true;
+ }
return false;
}
candidate_values.insert(
--- /dev/null
+/********************* */
+/*! \file sygus_repair_const.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of sygus_repair_const
+ **/
+
+#include "theory/quantifiers/sygus/sygus_repair_const.h"
+
+#include "options/base_options.h"
+#include "printer/printer.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
+#include "smt/smt_statistics_registry.h"
+#include "theory/quantifiers/cegqi/ceg_instantiator.h"
+#include "theory/quantifiers/sygus/term_database_sygus.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+SygusRepairConst::SygusRepairConst(QuantifiersEngine* qe)
+ : d_qe(qe), d_allow_constant_grammar(false)
+{
+ d_tds = d_qe->getTermDatabaseSygus();
+}
+
+void SygusRepairConst::initialize(Node base_inst,
+ const std::vector<Node>& candidates)
+{
+ Trace("sygus-repair-const") << "SygusRepairConst::initialize" << std::endl;
+ Trace("sygus-repair-const") << " conjecture : " << base_inst << std::endl;
+ d_base_inst = base_inst;
+
+ // compute whether there are "allow all constant" types in the variables of q
+ std::map<TypeNode, bool> tprocessed;
+ for (const Node& v : candidates)
+ {
+ TypeNode tn = v.getType();
+ // do the type traversal of the sygus type
+ registerSygusType(tn, tprocessed);
+ }
+ Trace("sygus-repair-const")
+ << " allow constants : " << d_allow_constant_grammar << std::endl;
+}
+
+// recursion depth bounded by number of types in grammar (small)
+void SygusRepairConst::registerSygusType(TypeNode tn,
+ std::map<TypeNode, bool>& tprocessed)
+{
+ if (tprocessed.find(tn) == tprocessed.end())
+ {
+ tprocessed[tn] = true;
+ Assert(tn.isDatatype());
+ const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+ Assert(dt.isSygus());
+ // check if this datatype allows all constants
+ if (dt.getSygusAllowConst())
+ {
+ d_allow_constant_grammar = true;
+ }
+ for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
+ {
+ const DatatypeConstructor& dtc = dt[i];
+ // recurse on all subfields
+ for (unsigned j = 0, nargs = dtc.getNumArgs(); j < nargs; j++)
+ {
+ TypeNode tnc = d_tds->getArgType(dtc, j);
+ registerSygusType(tnc, tprocessed);
+ }
+ }
+ }
+}
+
+bool SygusRepairConst::repairSolution(const std::vector<Node>& candidates,
+ const std::vector<Node>& candidate_values,
+ std::vector<Node>& repair_cv)
+{
+ Assert(candidates.size() == candidate_values.size());
+
+ // if no grammar type allows constants, no repair is possible
+ if (d_base_inst.isNull() || !d_allow_constant_grammar)
+ {
+ return false;
+ }
+ if (Trace.isOn("sygus-repair-const"))
+ {
+ Trace("sygus-repair-const") << "Repair candidate solutions..." << std::endl;
+ Printer* p = Printer::getPrinter(options::outputLanguage());
+ for (unsigned i = 0, size = candidates.size(); i < size; i++)
+ {
+ std::stringstream ss;
+ p->toStreamSygus(ss, candidate_values[i]);
+ Trace("sygus-repair-const")
+ << " " << candidates[i] << " -> " << ss.str() << std::endl;
+ }
+ Trace("sygus-repair-const")
+ << "Getting candidate skeletons : " << std::endl;
+ }
+ NodeManager* nm = NodeManager::currentNM();
+ std::vector<Node> candidate_skeletons;
+ std::map<TypeNode, int> free_var_count;
+ std::vector<Node> sk_vars;
+ std::map<Node, Node> sk_vars_to_subs;
+ for (unsigned i = 0, size = candidates.size(); i < size; i++)
+ {
+ Node cv = candidate_values[i];
+ Node skeleton = getSkeleton(cv, free_var_count, sk_vars, sk_vars_to_subs);
+ if (Trace.isOn("sygus-repair-const"))
+ {
+ Printer* p = Printer::getPrinter(options::outputLanguage());
+ std::stringstream ss;
+ p->toStreamSygus(ss, cv);
+ Trace("sygus-repair-const")
+ << "Solution #" << i << " : " << ss.str() << std::endl;
+ if (skeleton == cv)
+ {
+ Trace("sygus-repair-const") << "...solution unchanged" << std::endl;
+ }
+ else
+ {
+ std::stringstream sss;
+ p->toStreamSygus(sss, skeleton);
+ Trace("sygus-repair-const")
+ << "...inferred skeleton : " << sss.str() << std::endl;
+ }
+ }
+ candidate_skeletons.push_back(skeleton);
+ }
+
+ if (sk_vars.empty())
+ {
+ Trace("sygus-repair-const") << "...no solutions repaired." << std::endl;
+ return false;
+ }
+
+ Trace("sygus-repair-const") << "Get first-order query..." << std::endl;
+ Node fo_body = getFoQuery(candidates, candidate_skeletons, sk_vars);
+
+ Trace("sygus-repair-const-debug") << "...got : " << fo_body << std::endl;
+
+ if (d_queries.find(fo_body) != d_queries.end())
+ {
+ Trace("sygus-repair-const") << "...duplicate query." << std::endl;
+ return false;
+ }
+ d_queries.insert(fo_body);
+
+ // check whether it is not in the current logic, e.g. non-linear arithmetic.
+ // if so, undo replacements until it is in the current logic.
+ LogicInfo logic = smt::currentSmtEngine()->getLogicInfo();
+ if (logic.isTheoryEnabled(THEORY_ARITH) && logic.isLinear())
+ {
+ fo_body = fitToLogic(logic,
+ fo_body,
+ candidates,
+ candidate_skeletons,
+ sk_vars,
+ sk_vars_to_subs);
+ }
+
+ if (fo_body.isNull() || sk_vars.empty())
+ {
+ Trace("sygus-repair-const")
+ << "...all skeleton variables lead to bad logic." << std::endl;
+ return false;
+ }
+
+ Trace("sygus-repair-const") << "Make satisfiabily query..." << std::endl;
+ if (fo_body.getKind() == FORALL)
+ {
+ // must be a CBQI quantifier
+ CegHandledStatus hstatus = CegInstantiator::isCbqiQuant(fo_body, d_qe);
+ if (hstatus < CEG_HANDLED)
+ {
+ // abort if less than fully handled
+ Trace("sygus-repair-const") << "...first-order query is not handlable by "
+ "counterexample-guided instantiation."
+ << std::endl;
+ return false;
+ }
+
+ // do miniscoping explicitly
+ if (fo_body[1].getKind() == AND)
+ {
+ Node bvl = fo_body[0];
+ std::vector<Node> children;
+ for (const Node& conj : fo_body[1])
+ {
+ children.push_back(nm->mkNode(FORALL, bvl, conj));
+ }
+ fo_body = nm->mkNode(AND, children);
+ }
+ }
+
+ Trace("cegqi-engine") << "Repairing previous solution..." << std::endl;
+ // make the satisfiability query
+ SmtEngine repcChecker(nm->toExprManager());
+ repcChecker.setLogic(smt::currentSmtEngine()->getLogicInfo());
+ repcChecker.assertFormula(fo_body.toExpr());
+ Result r = repcChecker.checkSat();
+ Trace("sygus-repair-const") << "...got : " << r << std::endl;
+ if (r.asSatisfiabilityResult().isSat()
+ && !r.asSatisfiabilityResult().isUnknown())
+ {
+ std::vector<Node> sk_sygus_m;
+ for (const Node& v : sk_vars)
+ {
+ Node fov = d_sk_to_fo[v];
+ Node fov_m = Node::fromExpr(repcChecker.getValue(fov.toExpr()));
+ Trace("sygus-repair-const") << " " << fov << " = " << fov_m << std::endl;
+ // convert to sygus
+ Node fov_m_to_sygus = d_tds->getProxyVariable(v.getType(), fov_m);
+ sk_sygus_m.push_back(fov_m_to_sygus);
+ }
+ std::stringstream ss;
+ // convert back to sygus
+ for (unsigned i = 0, size = candidates.size(); i < size; i++)
+ {
+ Node csk = candidate_skeletons[i];
+ Node scsk = csk.substitute(
+ sk_vars.begin(), sk_vars.end(), sk_sygus_m.begin(), sk_sygus_m.end());
+ repair_cv.push_back(scsk);
+ if (Trace.isOn("sygus-repair-const") || Trace.isOn("cegqi-engine"))
+ {
+ std::stringstream sss;
+ Printer::getPrinter(options::outputLanguage())
+ ->toStreamSygus(sss, repair_cv[i]);
+ ss << " * " << candidates[i] << " -> " << sss.str() << std::endl;
+ }
+ }
+ Trace("cegqi-engine") << "...success:" << std::endl;
+ Trace("cegqi-engine") << ss.str();
+ Trace("sygus-repair-const")
+ << "Repaired constants in solution : " << std::endl;
+ Trace("sygus-repair-const") << ss.str();
+ return true;
+ }
+
+ Trace("cegqi-engine") << "...failed" << std::endl;
+
+ return false;
+}
+
+bool SygusRepairConst::isRepairableConstant(Node n)
+{
+ if (n.getKind() != APPLY_CONSTRUCTOR)
+ {
+ return false;
+ }
+ TypeNode tn = n.getType();
+ Assert(tn.isDatatype());
+ const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+ Assert(dt.isSygus());
+ if (dt.getSygusAllowConst())
+ {
+ Node op = n.getOperator();
+ unsigned cindex = Datatype::indexOf(op.toExpr());
+ if (dt[cindex].getNumArgs() == 0)
+ {
+ Node sygusOp = Node::fromExpr(dt[cindex].getSygusOp());
+ if (sygusOp.isConst())
+ {
+ return true;
+ }
+ }
+ }
+ return false;
+}
+
+Node SygusRepairConst::getSkeleton(Node n,
+ std::map<TypeNode, int>& free_var_count,
+ std::vector<Node>& sk_vars,
+ std::map<Node, Node>& sk_vars_to_subs)
+{
+ if (isRepairableConstant(n))
+ {
+ Node sk_var = d_tds->getFreeVarInc(n.getType(), free_var_count);
+ sk_vars.push_back(sk_var);
+ sk_vars_to_subs[sk_var] = n;
+ Trace("sygus-repair-const-debug")
+ << "Var to subs : " << sk_var << " -> " << n << std::endl;
+ return sk_var;
+ }
+ NodeManager* nm = NodeManager::currentNM();
+ // get the most general candidate skeleton of n
+ std::unordered_map<TNode, Node, TNodeHashFunction> visited;
+ std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+ std::vector<TNode> visit;
+ TNode cur;
+ visit.push_back(n);
+ do
+ {
+ cur = visit.back();
+ visit.pop_back();
+ it = visited.find(cur);
+
+ if (it == visited.end())
+ {
+ visited[cur] = Node::null();
+ visit.push_back(cur);
+ for (const Node& cn : cur)
+ {
+ visit.push_back(cn);
+ }
+ }
+ else if (it->second.isNull())
+ {
+ Node ret = cur;
+ bool childChanged = false;
+ std::vector<Node> children;
+ if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
+ {
+ children.push_back(cur.getOperator());
+ }
+ for (const Node& cn : cur)
+ {
+ Node child;
+ // if it is a constant over a type that allows all constants
+ if (isRepairableConstant(cn))
+ {
+ // replace it by the next free variable
+ child = d_tds->getFreeVarInc(cn.getType(), free_var_count);
+ sk_vars.push_back(child);
+ sk_vars_to_subs[child] = cn;
+ Trace("sygus-repair-const-debug")
+ << "Var to subs : " << child << " -> " << cn << std::endl;
+ }
+ else
+ {
+ it = visited.find(cn);
+ Assert(it != visited.end());
+ Assert(!it->second.isNull());
+ child = it->second;
+ }
+ childChanged = childChanged || cn != child;
+ children.push_back(child);
+ }
+ if (childChanged)
+ {
+ ret = nm->mkNode(cur.getKind(), children);
+ }
+ visited[cur] = ret;
+ }
+ } while (!visit.empty());
+ Assert(visited.find(n) != visited.end());
+ Assert(!visited.find(n)->second.isNull());
+ return visited[n];
+}
+
+Node SygusRepairConst::getFoQuery(const std::vector<Node>& candidates,
+ const std::vector<Node>& candidate_skeletons,
+ const std::vector<Node>& sk_vars)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ Node body = d_base_inst.negate();
+ Trace("sygus-repair-const") << " Substitute skeletons..." << std::endl;
+ body = body.substitute(candidates.begin(),
+ candidates.end(),
+ candidate_skeletons.begin(),
+ candidate_skeletons.end());
+ Trace("sygus-repair-const-debug") << " ...got : " << body << std::endl;
+
+ Trace("sygus-repair-const") << " Unfold the specification..." << std::endl;
+ body = d_tds->evaluateWithUnfolding(body);
+ Trace("sygus-repair-const-debug") << " ...got : " << body << std::endl;
+
+ Trace("sygus-repair-const") << " Introduce first-order vars..." << std::endl;
+ // now, we must replace all terms of the form eval( z_i, t1...tn ) with
+ // a fresh first-order variable w_i, where z_i is a variable introduced in
+ // the skeleton inference step (z_i is a variable in sk_vars).
+ std::unordered_map<TNode, Node, TNodeHashFunction> visited;
+ std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+ std::vector<TNode> visit;
+ TNode cur;
+ visit.push_back(body);
+ do
+ {
+ cur = visit.back();
+ visit.pop_back();
+ it = visited.find(cur);
+
+ if (it == visited.end())
+ {
+ visited[cur] = Node::null();
+ if (cur.getKind() == APPLY_UF && cur.getNumChildren() > 0)
+ {
+ Node v = cur[0];
+ if (std::find(sk_vars.begin(), sk_vars.end(), v) != sk_vars.end())
+ {
+ std::map<Node, Node>::iterator itf = d_sk_to_fo.find(v);
+ if (itf == d_sk_to_fo.end())
+ {
+ Node sk_fov = nm->mkSkolem("k", cur.getType());
+ d_sk_to_fo[v] = sk_fov;
+ d_fo_to_sk[sk_fov] = v;
+ visited[cur] = sk_fov;
+ Trace("sygus-repair-const-debug")
+ << "Map " << v << " -> " << sk_fov << std::endl;
+ }
+ else
+ {
+ visited[cur] = itf->second;
+ }
+ }
+ }
+ if (visited[cur].isNull())
+ {
+ visit.push_back(cur);
+ for (const Node& cn : cur)
+ {
+ visit.push_back(cn);
+ }
+ }
+ }
+ else if (it->second.isNull())
+ {
+ Node ret = cur;
+ bool childChanged = false;
+ std::vector<Node> children;
+ if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
+ {
+ children.push_back(cur.getOperator());
+ }
+ for (const Node& cn : cur)
+ {
+ it = visited.find(cn);
+ Assert(it != visited.end());
+ Assert(!it->second.isNull());
+ childChanged = childChanged || cn != it->second;
+ children.push_back(it->second);
+ }
+ if (childChanged)
+ {
+ ret = nm->mkNode(cur.getKind(), children);
+ }
+ visited[cur] = ret;
+ }
+ } while (!visit.empty());
+ Assert(visited.find(body) != visited.end());
+ Assert(!visited.find(body)->second.isNull());
+ Node fo_body = visited[body];
+ Trace("sygus-repair-const-debug") << " ...got : " << fo_body << std::endl;
+ return fo_body;
+}
+
+Node SygusRepairConst::fitToLogic(LogicInfo& logic,
+ Node n,
+ const std::vector<Node>& candidates,
+ std::vector<Node>& candidate_skeletons,
+ std::vector<Node>& sk_vars,
+ std::map<Node, Node>& sk_vars_to_subs)
+{
+ std::vector<Node> rm_var;
+ Node exc_var;
+ while (getFitToLogicExcludeVar(logic, n, exc_var))
+ {
+ if (exc_var.isNull())
+ {
+ return n;
+ }
+ Trace("sygus-repair-const") << "...exclude " << exc_var
+ << " due to logic restrictions." << std::endl;
+ TNode tvar = exc_var;
+ Assert(sk_vars_to_subs.find(exc_var) != sk_vars_to_subs.end());
+ TNode tsubs = sk_vars_to_subs[exc_var];
+ // revert the substitution
+ for (unsigned i = 0, size = candidate_skeletons.size(); i < size; i++)
+ {
+ candidate_skeletons[i] = candidate_skeletons[i].substitute(tvar, tsubs);
+ }
+ // remove the variable
+ sk_vars_to_subs.erase(exc_var);
+ std::vector<Node>::iterator it =
+ std::find(sk_vars.begin(), sk_vars.end(), exc_var);
+ Assert(it != sk_vars.end());
+ sk_vars.erase(it);
+ // reconstruct the query
+ n = getFoQuery(candidates, candidate_skeletons, sk_vars);
+ // reset the exclusion variable
+ exc_var = Node::null();
+ }
+ return Node::null();
+}
+
+bool SygusRepairConst::getFitToLogicExcludeVar(LogicInfo& logic,
+ Node n,
+ Node& exvar)
+{
+ bool restrictLA = logic.isTheoryEnabled(THEORY_ARITH) && logic.isLinear();
+
+ // should have at least one restriction
+ Assert(restrictLA);
+
+ std::unordered_set<TNode, TNodeHashFunction> visited;
+ std::unordered_set<TNode, TNodeHashFunction>::iterator it;
+ std::vector<TNode> visit;
+ TNode cur;
+ visit.push_back(n);
+ do
+ {
+ cur = visit.back();
+ visit.pop_back();
+ it = visited.find(cur);
+
+ if (it == visited.end())
+ {
+ visited.insert(cur);
+ if (restrictLA && cur.getKind() == NONLINEAR_MULT)
+ {
+ for (const Node& ccur : cur)
+ {
+ std::map<Node, Node>::iterator itf = d_fo_to_sk.find(ccur);
+ if (itf != d_fo_to_sk.end())
+ {
+ exvar = itf->second;
+ return true;
+ }
+ }
+ return false;
+ }
+ for (const Node& ccur : cur)
+ {
+ visit.push_back(ccur);
+ }
+ }
+ } while (!visit.empty());
+
+ return true;
+}
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file sygus_repair_const.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief sygus_repair_const
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H
+#define __CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H
+
+#include <unordered_set>
+#include "expr/node.h"
+#include "theory/logic_info.h"
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class CegConjecture;
+
+/** SygusRepairConst
+ *
+ * This module is used to repair portions of candidate solutions. In particular,
+ * given a synthesis conjecture:
+ * exists f. forall x. P( f, x )
+ * and a candidate solution f = \x. t[x,c] where c are constants, this function
+ * checks whether there exists a term of the form \x. t[x,c'] for some constants
+ * c' such that:
+ * forall x. P( (\x. t[x,c']), x ) [***]
+ * is satisfiable, where notice that the above formula after beta-reduction may
+ * be one in pure first-order logic in a decidable theory (say linear
+ * arithmetic). To check this, we invoke a separate instance of the SmtEngine
+ * within repairSolution(...) below, which if satisfiable gives us the
+ * valuation for c'.
+ */
+class SygusRepairConst
+{
+ public:
+ SygusRepairConst(QuantifiersEngine* qe);
+ ~SygusRepairConst() {}
+ /** initialize
+ *
+ * Initialize this class with the base instantiation of the sygus conjecture
+ * (see CegConjecture::d_base_inst) and its candidate variables (see
+ * CegConjecture::d_candidates).
+ */
+ void initialize(Node base_inst, const std::vector<Node>& candidates);
+ /** repair solution
+ *
+ * This function is called when candidates -> candidate_values is a (failed)
+ * candidate solution for the synthesis conjecture.
+ *
+ * If this function returns true, then this class adds to repair_cv the
+ * repaired version of the solution candidate_values for each candidate,
+ * where for each index i, repair_cv[i] is obtained by replacing constant
+ * subterms in candidate_values[i] with others, and
+ * candidates -> repair_cv
+ * is a solution for the synthesis conjecture associated with this class.
+ * Moreover, it is the case that
+ * repair_cv[j] != candidate_values[j], for at least one j.
+ */
+ bool repairSolution(const std::vector<Node>& candidates,
+ const std::vector<Node>& candidate_values,
+ std::vector<Node>& repair_cv);
+
+ private:
+ /** reference to quantifier engine */
+ QuantifiersEngine* d_qe;
+ /** pointer to the sygus term database of d_qe */
+ TermDbSygus* d_tds;
+ /**
+ * The "base instantiation" of the deep embedding form of the synthesis
+ * conjecture associated with this class, see CegConjecture::d_base_inst.
+ */
+ Node d_base_inst;
+ /**
+ * whether any sygus type for the candidate variables of d_base_inst (the
+ * syntactic restrictions) allows all constants. If this flag is false, then
+ * this class is a no-op.
+ */
+ bool d_allow_constant_grammar;
+ /** map from skeleton variables to first-order variables */
+ std::map<Node, Node> d_sk_to_fo;
+ /** reverse map of d_sk_to_fo */
+ std::map<Node, Node> d_fo_to_sk;
+ /** a cache of satisfiability queries of the form [***] above we have tried */
+ std::unordered_set<Node, NodeHashFunction> d_queries;
+ /**
+ * Register information for sygus type tn, tprocessed stores the set of
+ * already registered types.
+ */
+ void registerSygusType(TypeNode tn, std::map<TypeNode, bool>& tprocessed);
+ /**
+ * Returns true if n is a term of a sygus datatype type that allows all
+ * constants, and n encodes a constant. The term n must have a sygus datatype
+ * type.
+ */
+ bool isRepairableConstant(Node n);
+ /** get skeleton
+ *
+ * Returns a skeleton for n, where the subterms of n that are repairable
+ * constants are replaced by free variables. Since we are interested in
+ * returning canonical skeletons, the free variables we use in this
+ * replacement are taken from TermDbSygus, where we track indices
+ * in free_var_count. Variables we introduce in this way are added to sk_vars.
+ * The mapping sk_vars_to_subs contains entries v -> c, where v is a
+ * variable in sk_vars, and c is the term in n that it replaced.
+ */
+ Node getSkeleton(Node n,
+ std::map<TypeNode, int>& free_var_count,
+ std::vector<Node>& sk_vars,
+ std::map<Node, Node>& sk_vars_to_subs);
+ /** get first-order query
+ *
+ * This function returns a formula that is equivalent to the negation of the
+ * synthesis conjecture, where candidates are replaced by candidate_skeletons,
+ * whose free variables are in the set sk_vars. The returned formula
+ * is a first-order (quantified) formula in the background logic, without UF,
+ * of the form [***] above.
+ */
+ Node getFoQuery(const std::vector<Node>& candidates,
+ const std::vector<Node>& candidate_skeletons,
+ const std::vector<Node>& sk_vars);
+ /** fit to logic
+ *
+ * This function ensures that a query of the form [***] above fits the given
+ * logic. In our approach for constant repair, replacing constants by
+ * variables may introduce e.g. non-linearity. If non-linear arithmetic is
+ * not enabled, we must undo some of the variables we introduced when
+ * inferring candidate skeletons.
+ *
+ * This function may remove variables from sk_vars and the map
+ * sk_vars_to_subs. The skeletons candidate_skeletons are obtained by
+ * getSkeleton(...) on the resulting vectors. If this function returns a
+ * non-null node n', then n' is getFoQuery(...) on the resulting vectors, and
+ * n' is in the given logic. The function may return null if it is not
+ * possible to find a n' of this form.
+ *
+ * It uses the function below to choose which variables to remove from
+ * sk_vars.
+ */
+ Node fitToLogic(LogicInfo& logic,
+ Node n,
+ const std::vector<Node>& candidates,
+ std::vector<Node>& candidate_skeletons,
+ std::vector<Node>& sk_vars,
+ std::map<Node, Node>& sk_vars_to_subs);
+ /** get fit to logic exclusion variable
+ *
+ * If n is not in the given logic, then this method either returns false,
+ * or returns true and sets exvar to some variable in the domain of
+ * d_fo_to_sk, that must be replaced by a constant for n to be in the given
+ * logic. For example, for logic linear arithemic, for input:
+ * x * y = 5
+ * where x is in the domain of d_fo_to_sk, this function returns true and sets
+ * exvar to x.
+ * If n is in the given logic, this method returns true.
+ */
+ bool getFitToLogicExcludeVar(LogicInfo& logic, Node n, Node& exvar);
+};
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H */
std::map< Node, bool > visited;
return hasFreeVar( n, visited );
}
-
+
+Node TermDbSygus::getProxyVariable(TypeNode tn, Node c)
+{
+ Assert(tn.isDatatype());
+ Assert(static_cast<DatatypeType>(tn.toType()).getDatatype().isSygus());
+ Assert(
+ TypeNode::fromType(
+ static_cast<DatatypeType>(tn.toType()).getDatatype().getSygusType())
+ == c.getType());
+
+ std::map<Node, Node>::iterator it = d_proxy_vars[tn].find(c);
+ if (it == d_proxy_vars[tn].end())
+ {
+ Node k = NodeManager::currentNM()->mkSkolem("sy", tn, "sygus proxy");
+ SygusPrintProxyAttribute spa;
+ k.setAttribute(spa, c);
+ d_proxy_vars[tn][c] = k;
+ return k;
+ }
+ return it->second;
+}
+
TypeNode TermDbSygus::getSygusTypeForVar( Node v ) {
Assert( d_fv_stype.find( v )!=d_fv_stype.end() );
return d_fv_stype[v];
int getVarNum(Node n) { return d_fv_num[n]; }
/** returns true if n has a cached free variable (in d_fv). */
bool hasFreeVar(Node n);
+ /** get sygus proxy variable
+ *
+ * Returns a fresh variable of type tn with the SygusPrintProxyAttribute set
+ * to constant c. The type tn should be a sygus datatype type, and the type of
+ * c should be the analog type of tn. The semantics of the returned node
+ * is "the variable of sygus datatype tn that encodes constant c".
+ */
+ Node getProxyVariable(TypeNode tn, Node c);
/** make generic
*
* This function returns a builtin term f( t1, ..., tn ) where f is the
Node sygusToBuiltin(Node n, TypeNode tn);
/** same as above, but without tn */
Node sygusToBuiltin(Node n) { return sygusToBuiltin(n, n.getType()); }
+ /** evaluate builtin
+ *
+ * bn is a term of some sygus datatype tn. This function returns the rewritten
+ * form of bn [ args / vars(tn) ], where vars(tn) is the sygus variable
+ * list for type tn (see Datatype::getSygusVarList).
+ */
+ Node evaluateBuiltin(TypeNode tn, Node bn, std::vector<Node>& args);
+ /** evaluate with unfolding
+ *
+ * n is any term that may involve sygus evaluation functions. This function
+ * returns the result of unfolding the evaluation functions within n and
+ * rewriting the result. For example, if eval_A is the evaluation function
+ * for the datatype:
+ * A -> C_0 | C_1 | C_x | C_+( C_A, C_A )
+ * corresponding to grammar:
+ * A -> 0 | 1 | x | A + A
+ * then calling this function on eval( C_+( x, 1 ), 4 ) = y returns 5 = y.
+ * The node returned by this function is in (extended) rewritten form.
+ */
+ Node evaluateWithUnfolding(Node n);
+ /** same as above, but with a cache of visited nodes */
+ Node evaluateWithUnfolding(
+ Node n, std::unordered_map<Node, Node, NodeHashFunction>& visited);
//-----------------------------end conversion from sygus to builtin
private:
std::map<Node, int> d_fv_num;
/** recursive helper for hasFreeVar, visited stores nodes we have visited. */
bool hasFreeVar(Node n, std::map<Node, bool>& visited);
+ /** cache of getProxyVariable */
+ std::map<TypeNode, std::map<Node, Node> > d_proxy_vars;
//-----------------------------end conversion from sygus to builtin
// TODO :issue #1235 : below here needs refactor
return unfold( en, vtm, exp, false );
}
Node getEagerUnfold( Node n, std::map< Node, Node >& visited );
-
- // builtin evaluation, returns rewrite( bn [ args / vars(tn) ] )
- Node evaluateBuiltin( TypeNode tn, Node bn, std::vector< Node >& args );
- // evaluate with unfolding
- Node evaluateWithUnfolding(
- Node n, std::unordered_map<Node, Node, NodeHashFunction>& visited);
- Node evaluateWithUnfolding( Node n );
};
}/* CVC4::theory::quantifiers namespace */
regress1/sygus/clock-inc-tuple.sy \
regress1/sygus/commutative.sy \
regress1/sygus/constant.sy \
+ regress1/sygus/constant-ite-bv.sy \
regress1/sygus/dt-test-ns.sy \
regress1/sygus/dup-op.sy \
regress1/sygus/fg_polynomial3.sy \
--- /dev/null
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status --no-sygus-pbe --sygus-repair-const
+(set-logic BV)
+(synth-fun f ( (x (BitVec 64))) (BitVec 64)
+(
+(Start (BitVec 64) (
+ #x0000000000000000
+ #x0000000000000001
+ x
+ (bvnot Start)
+ (bvadd Start Start)
+ (ite StartBool Start Start)
+ (Constant (BitVec 64))
+ ))
+(StartBool Bool ((bvule Start Start)))
+)
+)
+(constraint (= (f #x6E393354DFFAAB51) #xC8E366559002AA57))
+(constraint (= (f #xFDA75AD598A27135) #xC8E366559002AA57))
+(constraint (= (f #x58682C0FA4F8DB6D) #xC8E366559002AA57))
+(constraint (= (f #x58FDC0941A7E079F) #xC8E366559002AA57))
+(constraint (= (f #xBDC9B88103ECB0C9) #xC8E366559002AA57))
+(constraint (= (f #x000000000001502F) #x0000000000000000))
+(constraint (= (f #x0000000000010999) #x0000000000000000))
+(constraint (= (f #x0000000000013169) #x0000000000000000))
+(constraint (= (f #x000000000001B1A9) #x0000000000000000))
+(constraint (= (f #x0000000000016D77) #x0000000000000000))
+(constraint (= (f #x0000000000000001) #x0000000000000000))
+(check-synth)
projects / cvc5.git / commitdiff