diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2018-05-17 14:47:30 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-17 14:47:30 -0500 |
commit | 6e3f8936d74ec2d2ed99b68cd77df771607c527f (patch) | |
tree | f3fdca01d16aa00cc12de116cefd25b00408e7c6 /src/theory/quantifiers/sygus/cegis_unif.cpp | |
parent | 19cf50fcb832b01bb119dc1cfc31884e4e864f06 (diff) |
Option to force return values of Bool functions to be constant in CegisUnif (#1930)
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis_unif.cpp')
-rw-r--r-- | src/theory/quantifiers/sygus/cegis_unif.cpp | 23 |
1 files changed, 4 insertions, 19 deletions
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 9ae598f83..692055b87 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -37,7 +37,6 @@ bool CegisUnif::processInitialize(Node n, const std::vector<Node>& candidates, std::vector<Node>& lemmas) { - Trace("cegis-unif") << "Initialize CegisUnif : " << n << std::endl; // list of strategy points for unification candidates std::vector<Node> unif_candidate_pts; // map from strategy points to their conditions @@ -453,24 +452,10 @@ void CegisUnifEnumManager::incrementNumEnumerators() << " to strategy point " << ci.second.d_pt << "\n"; d_tds->registerEnumerator(e, ci.second.d_pt, d_parent); - // if the sygus datatype is interpreted as an infinite type - // (this should be the case for almost all examples) - TypeNode et = e.getType(); - if (!et.isInterpretedFinite()) - { - // it is disequal from all previous ones - for (const Node& ei : ci.second.d_enums[index]) - { - if (ei == e) - { - continue; - } - Node deq = e.eqNode(ei).negate(); - Trace("cegis-unif-enum-lemma") - << "CegisUnifEnum::lemma, enum deq:" << deq << "\n"; - d_qe->getOutputChannel().lemma(deq); - } - } + // TODO symmetry breaking for making + // e distinct from ei : (ci.second.d_enums[index] \ {e}) + // if its respective type has had at least + // ci.second.d_enums[index].size() distinct values enumerated } } // register the evaluation points at the new value |