diff options
Diffstat (limited to 'src/theory')
4 files changed, 61 insertions, 8 deletions
diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp index 2eefff967..f279b4ff4 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp @@ -124,7 +124,7 @@ void CegConjecture::assign( Node q ) { // initialize the sygus constant repair utility if (options::sygusRepairConst()) { - d_sygus_rconst->initialize(d_base_inst, d_candidates); + d_sygus_rconst->initialize(d_base_inst.negate(), d_candidates); } // register this term with sygus database and other utilities that impact diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index 4aaccc71e..b35fa5437 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -415,7 +415,7 @@ Node SygusRepairConst::getFoQuery(const std::vector<Node>& candidates, const std::vector<Node>& sk_vars) { NodeManager* nm = NodeManager::currentNM(); - Node body = d_base_inst.negate(); + Node body = d_base_inst; Trace("sygus-repair-const") << " Substitute skeletons..." << std::endl; body = body.substitute(candidates.begin(), candidates.end(), diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index 6b7d34cc9..57d12e3e1 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -674,7 +674,7 @@ Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons, << " add condition (" << c_counter << "/" << d_conds.size() << "): " << ce << " -> " << ss.str() << std::endl; } - cv = repairCondition(cv,e,er); + //cv = repairConditionToSeparate(ce, cv,e,er); d_conds[c_counter] = cv; // cache the separation class std::vector<Node> prev_sep_c = d_pt_sep.d_trie.d_rep_to_class[er]; @@ -828,11 +828,64 @@ Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons, return cache[root]; } -Node SygusUnifRl::DecisionTreeInfo::repairCondition( Node cond, Node e1, Node e2 ) +Node SygusUnifRl::DecisionTreeInfo::repairConditionToSeparate( Node ce, Node cv, Node e1, Node e2 ) { // repair condition - - return cond; + if( options::sygusRepairConst() ) + { + if( SygusRepairConst::mustRepair(cv) ) + { + SygusRepairConst src(d_unif->d_qe); + Node t[2]; + for( unsigned i=0; i<2; i++ ) + { + Node ei = i==0 ? e1 : e2; + std::map<Node, std::vector<Node>>::iterator it = d_unif->d_hd_to_pt.find(ei); + Assert( it != d_unif->d_hd_to_pt.end() ); + std::vector< Node > children; + children.push_back(ce); + children.insert(children.end(),it->second.begin(),it->second.end()); + t[i] = datatypes::DatatypesRewriter::mkSygusEvalApp(children); + } + Node deq = t[0].eqNode(t[1]).negate(); + Trace("sygus-unif-sol") << "Try to repair to satisfy : " << deq << std::endl; + std::vector< Node > candidate; + candidate.push_back(ce); + std::vector< Node > candidate_value; + candidate_value.push_back(cv); + src.initialize(deq,candidate); + std::vector< Node > repair_cv; + if(src.repairSolution(candidate,candidate_value,repair_cv)) + { + Assert(repair_cv.size()==1); + Node cvr = repair_cv[0]; + if(Trace.isOn("sygus-unif-sol")) + { + Trace("sygus-unif-sol") << "Repaired "; + std::stringstream ss; + Printer::getPrinter(options::outputLanguage()) + ->toStreamSygus(ss, cv); + Trace("sygus-unif-sol") << ss.str() << " to "; + std::stringstream ssr; + Printer::getPrinter(options::outputLanguage()) + ->toStreamSygus(ssr, cvr); + Trace("sygus-unif-sol") << ssr.str() << " to separate points:\n"; + for( unsigned i=0; i<2; i++ ) + { + Node ei = i==0 ? e1 : e2; + std::map<Node, std::vector<Node>>::iterator it = d_unif->d_hd_to_pt.find(ei); + Trace("sygus-unif-sol") << " " << it->second << std::endl; + } + } + return cvr; + } + else + { + Trace("sygus-unif-sol") << "...failed." << std::endl; + } + } + } + return cv; } void SygusUnifRl::DecisionTreeInfo::PointSeparator::initialize( diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h index feb227002..0b1b94dd2 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.h +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h @@ -279,8 +279,8 @@ class SygusUnifRl : public SygusUnif /** reference to parent unif util */ DecisionTreeInfo* d_dt; }; - /** repair condition */ - Node repairCondition( Node cond, Node e1, Node e2 ); + /** repair condition to separate */ + Node repairConditionToSeparate( Node ce, Node cv, Node e1, Node e2 ); /** * Utility for determining how evaluation points are separated by currently * enumerated condiotion values |