From: Andrew Reynolds Date: Thu, 10 May 2018 21:48:51 +0000 (-0500) Subject: Sygus repair constants (#1812) X-Git-Tag: cvc5-1.0.0~5065 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=adcbee78823120baa47eb8ba868b614512a121a9;p=cvc5.git Sygus repair constants (#1812) --- diff --git a/src/Makefile.am b/src/Makefile.am index 28333d905..17deeba81 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -493,6 +493,8 @@ libcvc4_la_SOURCES = \ 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 \ diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 4c771c143..10000bbb1 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -976,6 +976,14 @@ header = "options/quantifiers_options.h" 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" diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index ac5563fb3..c40096e3f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1318,6 +1318,11 @@ void SmtEngine::setDefaults() { options::cbqiMidpoint.set(true); } } + else + { + // cannot use sygus repair constants + options::sygusRepairConst.set(false); + } if(options::forceLogicString.wasSetByUser()) { d_logic = LogicInfo(options::forceLogicString()); @@ -1485,7 +1490,8 @@ void SmtEngine::setDefaults() { // 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")); @@ -5378,6 +5384,11 @@ void SmtEngine::checkSynthSolution() map 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 function_vars, function_sols; for (const auto& pair : sol_map) @@ -5462,8 +5473,8 @@ void SmtEngine::checkSynthSolution() 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(); } diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index 757f4d040..15c071431 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -1122,7 +1122,8 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) { 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; diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp index c52d22cdb..98a493423 100644 --- a/src/theory/quantifiers/extended_rewrite.cpp +++ b/src/theory/quantifiers/extended_rewrite.cpp @@ -771,8 +771,14 @@ Node ExtendedRewriter::extendedRewriteEqRes(Kind andk, 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 @@ -1070,8 +1076,6 @@ bool ExtendedRewriter::inferSubstitution(Node n, { n = slv_eq; } - NodeManager* nm = NodeManager::currentNM(); - Node v[2]; for (unsigned i = 0; i < 2; i++) { diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp index 69cf7f73b..cc12fdf17 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp @@ -41,10 +41,12 @@ CegConjecture::CegConjecture(QuantifiersEngine* qe) 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) { @@ -116,6 +118,12 @@ void CegConjecture::assign( Node q ) { 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; @@ -243,14 +251,45 @@ void CegConjecture::doCheck(std::vector& lems) std::vector 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 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 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 enum_values; getModelValues(terms, enum_values); - std::vector 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(); diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.h b/src/theory/quantifiers/sygus/ce_guided_conjecture.h index 97cc9df1e..231f9f14e 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.h +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.h @@ -27,6 +27,8 @@ #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 { @@ -118,10 +120,12 @@ public: /** 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); @@ -136,6 +140,8 @@ private: std::unique_ptr d_ceg_proc; /** grammar utility */ std::unique_ptr d_ceg_gc; + /** repair constant utility */ + std::unique_ptr d_sygus_rconst; //------------------------modules /** program by examples module */ @@ -160,7 +166,8 @@ private: 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 */ @@ -185,7 +192,12 @@ private: /** list of terms we have instantiated candidates with */ std::vector< Node > d_inst; }; - std::map< Node, CandidateInfo > d_cinfo; + std::map 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 */ diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp index 86f5abf61..0aebbe11a 100644 --- a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp @@ -201,10 +201,6 @@ void CegInstantiation::getSynthSolutions(std::map& sol_map) { d_conj->getSynthSolutions(sol_map, d_last_inst_si); } - else - { - Assert(false); - } } void CegInstantiation::preregisterAssertion( Node n ) { diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp index c37c0a57a..24b57d025 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp @@ -1220,10 +1220,7 @@ Node CegConjectureSingleInvSol::builtinToSygusConst(Node c, // 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 { diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index f48955c9f..92fea9586 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -134,6 +134,13 @@ bool Cegis::constructCandidates(const std::vector& enums, { if (addEvalLemmas(enums, enum_values)) { + // it may be repairable + SygusRepairConst* src = d_parent->getRepairConst(); + std::vector fail_cvs = enum_values; + if (src->repairSolution(candidates, fail_cvs, candidate_values)) + { + return true; + } return false; } candidate_values.insert( diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp new file mode 100644 index 000000000..1ca1902a1 --- /dev/null +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -0,0 +1,543 @@ +/********************* */ +/*! \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& 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 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& tprocessed) +{ + if (tprocessed.find(tn) == tprocessed.end()) + { + tprocessed[tn] = true; + Assert(tn.isDatatype()); + const Datatype& dt = static_cast(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& candidates, + const std::vector& candidate_values, + std::vector& 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 candidate_skeletons; + std::map free_var_count; + std::vector sk_vars; + std::map 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 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 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(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& free_var_count, + std::vector& sk_vars, + std::map& 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 visited; + std::unordered_map::iterator it; + std::vector 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 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& candidates, + const std::vector& candidate_skeletons, + const std::vector& 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 visited; + std::unordered_map::iterator it; + std::vector 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::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 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& candidates, + std::vector& candidate_skeletons, + std::vector& sk_vars, + std::map& sk_vars_to_subs) +{ + std::vector 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::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 visited; + std::unordered_set::iterator it; + std::vector 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::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 */ diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h new file mode 100644 index 000000000..b2a0d888d --- /dev/null +++ b/src/theory/quantifiers/sygus/sygus_repair_const.h @@ -0,0 +1,176 @@ +/********************* */ +/*! \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 +#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& 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& candidates, + const std::vector& candidate_values, + std::vector& 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 d_sk_to_fo; + /** reverse map of d_sk_to_fo */ + std::map d_fo_to_sk; + /** a cache of satisfiability queries of the form [***] above we have tried */ + std::unordered_set d_queries; + /** + * Register information for sygus type tn, tprocessed stores the set of + * already registered types. + */ + void registerSygusType(TypeNode tn, std::map& 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& free_var_count, + std::vector& sk_vars, + std::map& 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& candidates, + const std::vector& candidate_skeletons, + const std::vector& 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& candidates, + std::vector& candidate_skeletons, + std::vector& sk_vars, + std::map& 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 */ diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index c8d7bf04d..3121a4253 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -104,7 +104,28 @@ bool TermDbSygus::hasFreeVar( Node n ) { std::map< Node, bool > visited; return hasFreeVar( n, visited ); } - + +Node TermDbSygus::getProxyVariable(TypeNode tn, Node c) +{ + Assert(tn.isDatatype()); + Assert(static_cast(tn.toType()).getDatatype().isSygus()); + Assert( + TypeNode::fromType( + static_cast(tn.toType()).getDatatype().getSygusType()) + == c.getType()); + + std::map::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]; diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index 57a127d8d..f108dfb8e 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -128,6 +128,14 @@ class TermDbSygus { 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 @@ -152,6 +160,29 @@ class TermDbSygus { 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& 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& visited); //-----------------------------end conversion from sygus to builtin private: @@ -201,6 +232,8 @@ class TermDbSygus { std::map d_fv_num; /** recursive helper for hasFreeVar, visited stores nodes we have visited. */ bool hasFreeVar(Node n, std::map& visited); + /** cache of getProxyVariable */ + std::map > d_proxy_vars; //-----------------------------end conversion from sygus to builtin // TODO :issue #1235 : below here needs refactor @@ -316,13 +349,6 @@ public: 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& visited); - Node evaluateWithUnfolding( Node n ); }; }/* CVC4::theory::quantifiers namespace */ diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index c3de09de2..52eb63789 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1474,6 +1474,7 @@ REG1_TESTS = \ 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 \ diff --git a/test/regress/regress1/sygus/constant-ite-bv.sy b/test/regress/regress1/sygus/constant-ite-bv.sy new file mode 100644 index 000000000..330ef026e --- /dev/null +++ b/test/regress/regress1/sygus/constant-ite-bv.sy @@ -0,0 +1,29 @@ +; 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)