diff options
| -rw-r--r-- | src/smt/smt_engine.cpp | 27 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis.cpp | 35 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis.h | 2 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_repair_const.cpp | 28 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_repair_const.h | 29 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/coeff-solve-inv.sy | 29 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/repair-const-rl.sy | 24 |
8 files changed, 136 insertions, 40 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 62b4dc121..29c3f9092 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -510,8 +510,6 @@ class SmtEnginePrivate : public NodeManagerListener { * universally quantified in the constraints. */ std::vector<Node> d_sygusVars; - /** types of sygus primed variables (for debugging) */ - std::vector<Type> d_sygusPrimedVarTypes; /** sygus constraints */ std::vector<Node> d_sygusConstraints; /** functions-to-synthesize */ @@ -3925,9 +3923,7 @@ void SmtEngine::declareSygusVar(const std::string& id, Expr var, Type type) void SmtEngine::declareSygusPrimedVar(const std::string& id, Type type) { -#ifdef CVC4_ASSERTIONS - d_private->d_sygusPrimedVarTypes.push_back(type); -#endif + // do nothing (the command is spurious) Trace("smt") << "SmtEngine::declareSygusPrimedVar: " << id << "\n"; // don't need to set that the conjecture is stale } @@ -4010,27 +4006,6 @@ void SmtEngine::assertSygusInvConstraint(const Expr& inv, ss << vars.back() << "'"; primed_vars.push_back(d_nodeManager->mkBoundVar(ss.str(), tn)); d_private->d_sygusVars.push_back(primed_vars.back()); -#ifdef CVC4_ASSERTIONS - bool find_new_declared_var = false; - for (const Type& t : d_private->d_sygusPrimedVarTypes) - { - if (t == ti) - { - d_private->d_sygusPrimedVarTypes.erase( - std::find(d_private->d_sygusPrimedVarTypes.begin(), - d_private->d_sygusPrimedVarTypes.end(), - t)); - find_new_declared_var = true; - break; - } - } - if (!find_new_declared_var) - { - Warning() - << "warning: declared primed variables do not match invariant's " - "type\n"; - } -#endif } // make relevant terms; 0 -> Inv, 1 -> Pre, 2 -> Trans, 3 -> Post diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 96f347890..3a1ddc73c 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -198,6 +198,30 @@ bool Cegis::addEvalLemmas(const std::vector<Node>& candidates, return addedEvalLemmas; } +Node Cegis::getRefinementLemmaFormula() +{ + std::vector<Node> conj; + conj.insert( + conj.end(), d_refinement_lemmas.begin(), d_refinement_lemmas.end()); + // get the propagated values + for (unsigned i = 0, nprops = d_rl_eval_hds.size(); i < nprops; i++) + { + conj.push_back(d_rl_eval_hds[i].eqNode(d_rl_vals[i])); + } + // make the formula + NodeManager* nm = NodeManager::currentNM(); + Node ret; + if (conj.empty()) + { + ret = nm->mkConst(true); + } + else + { + ret = conj.size() == 1 ? conj[0] : nm->mkNode(AND, conj); + } + return ret; +} + bool Cegis::constructCandidates(const std::vector<Node>& enums, const std::vector<Node>& enum_values, const std::vector<Node>& candidates, @@ -235,11 +259,18 @@ bool Cegis::constructCandidates(const std::vector<Node>& enums, { std::vector<Node> fail_cvs = enum_values; Assert(candidates.size() == fail_cvs.size()); + // try to solve entire problem? if (src->repairSolution(candidates, fail_cvs, candidate_values)) { return true; } - // repair solution didn't work, exclude this solution + Node rl = getRefinementLemmaFormula(); + // try to solve for the refinement lemmas only + bool ret = + src->repairSolution(rl, candidates, fail_cvs, candidate_values); + // Even if ret is true, we will exclude the skeleton as well; this means + // that we have one chance to repair each skeleton. It is possible however + // that we might want to repair the same skeleton multiple times. std::vector<Node> exp; for (unsigned i = 0, size = enums.size(); i < size; i++) { @@ -252,7 +283,7 @@ bool Cegis::constructCandidates(const std::vector<Node>& enums, // must guard it expn = nm->mkNode(OR, d_parent->getGuard().negate(), expn.negate()); lems.push_back(expn); - return false; + return ret; } } diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index 891379992..08cf98c99 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -168,6 +168,8 @@ class Cegis : public SygusModule bool addEvalLemmas(const std::vector<Node>& candidates, const std::vector<Node>& candidate_values, std::vector<Node>& lems); + /** Get the node corresponding to the conjunction of all refinement lemmas. */ + Node getRefinementLemmaFormula(); //-----------------------------------end refinement lemmas /** Get refinement evaluation lemmas diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index 4c5baa4bb..39506b593 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -149,6 +149,19 @@ bool SygusRepairConst::repairSolution(const std::vector<Node>& candidates, std::vector<Node>& repair_cv, bool useConstantsAsHoles) { + return repairSolution(d_base_inst, + candidates, + candidate_values, + repair_cv, + useConstantsAsHoles); +} + +bool SygusRepairConst::repairSolution(Node sygusBody, + const std::vector<Node>& candidates, + const std::vector<Node>& candidate_values, + std::vector<Node>& repair_cv, + bool useConstantsAsHoles) +{ Assert(candidates.size() == candidate_values.size()); // if no grammar type allows constants, no repair is possible @@ -209,7 +222,8 @@ bool SygusRepairConst::repairSolution(const std::vector<Node>& candidates, NodeManager* nm = NodeManager::currentNM(); Trace("sygus-repair-const") << "Get first-order query..." << std::endl; - Node fo_body = getFoQuery(candidates, candidate_skeletons, sk_vars); + Node fo_body = + getFoQuery(sygusBody, candidates, candidate_skeletons, sk_vars); Trace("sygus-repair-const-debug") << "...got : " << fo_body << std::endl; @@ -225,7 +239,8 @@ bool SygusRepairConst::repairSolution(const std::vector<Node>& candidates, LogicInfo logic = smt::currentSmtEngine()->getLogicInfo(); if (logic.isTheoryEnabled(THEORY_ARITH) && logic.isLinear()) { - fo_body = fitToLogic(logic, + fo_body = fitToLogic(sygusBody, + logic, fo_body, candidates, candidate_skeletons, @@ -460,12 +475,12 @@ Node SygusRepairConst::getSkeleton(Node n, return visited[n]; } -Node SygusRepairConst::getFoQuery(const std::vector<Node>& candidates, +Node SygusRepairConst::getFoQuery(Node body, + 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; Trace("sygus-repair-const") << " Substitute skeletons..." << std::endl; body = body.substitute(candidates.begin(), candidates.end(), @@ -558,7 +573,8 @@ Node SygusRepairConst::getFoQuery(const std::vector<Node>& candidates, return fo_body; } -Node SygusRepairConst::fitToLogic(LogicInfo& logic, +Node SygusRepairConst::fitToLogic(Node body, + LogicInfo& logic, Node n, const std::vector<Node>& candidates, std::vector<Node>& candidate_skeletons, @@ -590,7 +606,7 @@ Node SygusRepairConst::fitToLogic(LogicInfo& logic, Assert(it != sk_vars.end()); sk_vars.erase(it); // reconstruct the query - n = getFoQuery(candidates, candidate_skeletons, sk_vars); + n = getFoQuery(body, candidates, candidate_skeletons, sk_vars); // reset the exclusion variable exc_var = Node::null(); } diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h index 26b7234a9..6be5ce5e6 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.h +++ b/src/theory/quantifiers/sygus/sygus_repair_const.h @@ -53,9 +53,9 @@ class SygusRepairConst ~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). + * Initialize this class with the base instantiation (body) of the sygus + * conjecture (see SynthConjecture::d_base_inst) and its candidate variables + * (see SynthConjecture::d_candidates). */ void initialize(Node base_inst, const std::vector<Node>& candidates); /** repair solution @@ -75,6 +75,17 @@ class SygusRepairConst * candidate_values to be repairable. In addition, if the flag * useConstantsAsHoles is true, we consider all constants whose (sygus) type * admit alls constants to be repairable. + * The repaired solution has the property that it satisfies the synthesis + * conjecture whose body is given by sygusBody. + */ + bool repairSolution(Node sygusBody, + const std::vector<Node>& candidates, + const std::vector<Node>& candidate_values, + std::vector<Node>& repair_cv, + bool useConstantsAsHoles = false); + /** + * Same as above, but where sygusBody is the body (base_inst) provided to the + * call to initialize of this class. */ bool repairSolution(const std::vector<Node>& candidates, const std::vector<Node>& candidate_values, @@ -148,12 +159,14 @@ class SygusRepairConst /** 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, + * synthesis conjecture whose body is given in the first argument, 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, + Node getFoQuery(Node body, + const std::vector<Node>& candidates, const std::vector<Node>& candidate_skeletons, const std::vector<Node>& sk_vars); /** fit to logic @@ -164,6 +177,9 @@ class SygusRepairConst * not enabled, we must undo some of the variables we introduced when * inferring candidate skeletons. * + * body is the (sygus) form of the original synthesis conjecture we are + * considering in this call. + * * 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 @@ -174,7 +190,8 @@ class SygusRepairConst * It uses the function below to choose which variables to remove from * sk_vars. */ - Node fitToLogic(LogicInfo& logic, + Node fitToLogic(Node body, + LogicInfo& logic, Node n, const std::vector<Node>& candidates, std::vector<Node>& candidate_skeletons, diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index cbe5f2e35..8dba70f91 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1669,6 +1669,7 @@ set(regress_1_tests regress1/sygus/cegisunif-depth1.sy regress1/sygus/cggmp.sy regress1/sygus/clock-inc-tuple.sy + regress1/sygus/coeff-solve-inv.sy regress1/sygus/commutative-stream.sy regress1/sygus/commutative.sy regress1/sygus/concat_extract_example.sy @@ -1726,6 +1727,7 @@ set(regress_1_tests regress1/sygus/qe.sy regress1/sygus/qf_abv.smt2 regress1/sygus/real-grammar.sy + regress1/sygus/repair-const-rl.sy regress1/sygus/repair-const-unk.sy regress1/sygus/simple-regexp.sy regress1/sygus/stopwatch-bt.sy diff --git a/test/regress/regress1/sygus/coeff-solve-inv.sy b/test/regress/regress1/sygus/coeff-solve-inv.sy new file mode 100644 index 000000000..edfcd6089 --- /dev/null +++ b/test/regress/regress1/sygus/coeff-solve-inv.sy @@ -0,0 +1,29 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status --sygus-repair-const --lang=sygus2 +(set-logic LIA) + +(synth-inv inv-f ((x Int) (y Int)) ) + + +(define-fun pre-f ((x Int) (y Int)) Bool + (and + (= x 0) + (= y 100) + ) +) + +(define-fun trans-f ((x Int) (y Int) (x! Int) (y! Int)) Bool + (and + (< x 100) + (= x! (+ x 1)) + (= y! (+ y 1)) + ) +) + +(define-fun post-f ((x Int) (y Int)) Bool + (=> (>= x 100) (>= y 200)) +) + +(inv-constraint inv-f pre-f trans-f post-f) + +(check-synth) diff --git a/test/regress/regress1/sygus/repair-const-rl.sy b/test/regress/regress1/sygus/repair-const-rl.sy new file mode 100644 index 000000000..6477de3fc --- /dev/null +++ b/test/regress/regress1/sygus/repair-const-rl.sy @@ -0,0 +1,24 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status --cegqi-si=none --sygus-repair-const --lang=sygus2 +(set-logic LIA) + +(synth-fun f ((x Int) (y Int)) Int + ((Start Int) (CInt Int)) + ( + (Start Int ((+ (* CInt x) (* CInt y) CInt))) + (CInt Int ((Constant Int))) + ) +) + +(declare-var x Int) +(declare-var y Int) + +(constraint (= (f 0 0) 100)) + +(constraint (= (f 1 1) 110)) + +(constraint (= (f 2 1) 117)) + +(constraint (>= (- (* 3 (f x y)) (f (* 2 x) (+ y 1))) (+ (* 7 x) (* 6 y)))) + +(check-synth) |