diff options
-rw-r--r-- | src/theory/quantifiers/sygus/cegis_unif.cpp | 23 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/cegis_unif.h | 4 | ||||
-rw-r--r-- | test/regress/regress0/sygus/let-ringer.sy | 1 |
3 files changed, 19 insertions, 9 deletions
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 57c4c1ad3..5a383a17a 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -53,9 +53,11 @@ bool CegisUnif::processInitialize(Node n, { Trace("cegis-unif") << "* non-unification candidate : " << f << std::endl; d_tds->registerEnumerator(f, f, d_parent); + d_non_unif_candidates.push_back(f); } else { + d_unif_candidates.push_back(f); Trace("cegis-unif") << "* unification candidate : " << f << " with strategy points:" << std::endl; std::vector<Node>& enums = d_cand_to_strat_pt[f]; @@ -80,14 +82,11 @@ bool CegisUnif::processInitialize(Node n, void CegisUnif::getTermList(const std::vector<Node>& candidates, std::vector<Node>& enums) { - for (const Node& c : candidates) + // Non-unif candidate are themselves the enumerators + enums.insert( + enums.end(), d_non_unif_candidates.begin(), d_non_unif_candidates.end()); + for (const Node& c : d_unif_candidates) { - // Non-unif candidate are themselves the enumerators - if (!d_sygus_unif.usingUnif(c)) - { - enums.push_back(c); - continue; - } // Collect heads of candidates for (const Node& hd : d_sygus_unif.getEvalPointHeads(c)) { @@ -105,6 +104,12 @@ bool CegisUnif::processConstructCandidates(const std::vector<Node>& enums, bool satisfiedRl, std::vector<Node>& lems) { + if (d_unif_candidates.empty()) + { + Assert(d_non_unif_candidates.size() == candidates.size()); + return Cegis::processConstructCandidates( + enums, enum_values, candidates, candidate_values, satisfiedRl, lems); + } if (!satisfiedRl) { // if we didn't satisfy the specification, there is no way to repair @@ -117,7 +122,7 @@ bool CegisUnif::processConstructCandidates(const std::vector<Node>& enums, Node cost_lit = d_u_enum_manager.getCurrentLiteral(); std::map<Node, std::vector<Node>> unif_enums[2]; std::map<Node, std::vector<Node>> unif_values[2]; - for (const Node& c : candidates) + for (const Node& c : d_unif_candidates) { // for each decision tree strategy allocated for c (these are referenced // by strategy points in d_cand_to_strat_pt[c]) @@ -196,7 +201,7 @@ bool CegisUnif::processConstructCandidates(const std::vector<Node>& enums, return false; } // set the conditions - for (const Node& c : candidates) + for (const Node& c : d_unif_candidates) { for (const Node& e : d_cand_to_strat_pt[c]) { diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index 80c11f82d..ec338a8b2 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -277,6 +277,10 @@ class CegisUnif : public Cegis CegisUnifEnumManager d_u_enum_manager; /* The null node */ Node d_null; + /** the unification candidates */ + std::vector<Node> d_unif_candidates; + /** the non-unification candidates */ + std::vector<Node> d_non_unif_candidates; /** list of strategy points per candidate */ std::map<Node, std::vector<Node>> d_cand_to_strat_pt; /** map from conditional enumerators to their strategy point */ diff --git a/test/regress/regress0/sygus/let-ringer.sy b/test/regress/regress0/sygus/let-ringer.sy index d26edffd2..0fe8dd05e 100644 --- a/test/regress/regress0/sygus/let-ringer.sy +++ b/test/regress/regress0/sygus/let-ringer.sy @@ -1,5 +1,6 @@ ; EXPECT: unsat ; COMMAND-LINE: --cegqi-si=all --sygus-out=status +; COMMAND-LINE: --cegqi-si=all --sygus-unif --sygus-out=status (set-logic LIA) (define-fun g ((x Int)) Int (ite (= x 1) 15 19)) (synth-fun f ((x Int)) Int |