summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/CMakeLists.txt6
-rw-r--r--src/theory/quantifiers/sygus/cegis.cpp49
-rw-r--r--src/theory/quantifiers/sygus/cegis.h14
-rw-r--r--src/theory/quantifiers/sygus/synth_conjecture.cpp41
-rw-r--r--src/theory/quantifiers/sygus/synth_conjecture.h15
5 files changed, 121 insertions, 4 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 26cc5bbcc..f0aee982c 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -562,6 +562,12 @@ libcvc4_add_sources(
theory/quantifiers/sygus/cegis_core_connective.h
theory/quantifiers/sygus/cegis_unif.cpp
theory/quantifiers/sygus/cegis_unif.h
+ theory/quantifiers/sygus/example_eval_cache.cpp
+ theory/quantifiers/sygus/example_eval_cache.h
+ theory/quantifiers/sygus/example_infer.cpp
+ theory/quantifiers/sygus/example_infer.h
+ theory/quantifiers/sygus/example_min_eval.cpp
+ theory/quantifiers/sygus/example_min_eval.h
theory/quantifiers/sygus/enum_stream_substitution.cpp
theory/quantifiers/sygus/enum_stream_substitution.h
theory/quantifiers/sygus/example_infer.cpp
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index 2d27878fd..f7d0e7b7e 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -426,6 +426,7 @@ void Cegis::addRefinementLemmaConjunct(unsigned wcounter,
d_rl_eval_hds.push_back(term);
d_rl_vals.push_back(val);
d_refinement_lemma_unit.insert(lem);
+
// apply to waiting lemmas beyond this one
for (unsigned i = wcounter + 1, size = waiting.size(); i < size; i++)
{
@@ -573,6 +574,54 @@ bool Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs,
return ret;
}
+bool Cegis::checkRefinementEvalLemmas(const std::vector<Node>& vs,
+ const std::vector<Node>& ms)
+{
+ // Maybe we already evaluated some terms in refinement lemmas.
+ // In particular, the example eval cache for f may have some evaluations
+ // cached, which we add to evalVisited and pass to the evaluator below.
+ std::unordered_map<Node, Node, NodeHashFunction> evalVisited;
+ ExampleInfer* ei = d_parent->getExampleInfer();
+ for (unsigned i = 0, vsize = vs.size(); i < vsize; i++)
+ {
+ Node f = vs[i];
+ ExampleEvalCache* eec = d_parent->getExampleEvalCache(f);
+ if (eec != nullptr)
+ {
+ // get the results we obtained through the example evaluation utility
+ std::vector<Node> vsProc;
+ std::vector<Node> msProc;
+ Node bmsi = d_tds->sygusToBuiltin(ms[i]);
+ ei->getExampleTerms(f, vsProc);
+ eec->evaluateVec(bmsi, msProc);
+ Assert(vsProc.size() == msProc.size());
+ for (unsigned j = 0, psize = vsProc.size(); j < psize; j++)
+ {
+ evalVisited[vsProc[j]] = msProc[j];
+ Assert(vsProc[j].getType() == msProc[j].getType());
+ }
+ }
+ }
+
+ Evaluator* eval = d_tds->getEvaluator();
+ for (unsigned r = 0; r < 2; r++)
+ {
+ std::unordered_set<Node, NodeHashFunction>& rlemmas =
+ r == 0 ? d_refinement_lemma_unit : d_refinement_lemma_conj;
+ for (const Node& lem : rlemmas)
+ {
+ // We may have computed the evaluation of some function applications
+ // via example-based symmetry breaking, stored in evalVisited.
+ Node lemcsu = eval->eval(lem, vs, ms, evalVisited);
+ if (lemcsu.isConst() && !lemcsu.getConst<bool>())
+ {
+ return true;
+ }
+ }
+ }
+ return false;
+}
+
bool Cegis::sampleAddRefinementLemma(const std::vector<Node>& candidates,
const std::vector<Node>& vals,
std::vector<Node>& lems)
diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h
index adaecc7f6..2c21257b9 100644
--- a/src/theory/quantifiers/sygus/cegis.h
+++ b/src/theory/quantifiers/sygus/cegis.h
@@ -114,6 +114,7 @@ class Cegis : public SygusModule
std::vector<Node> d_rl_vals;
/** all variables appearing in refinement lemmas */
std::unordered_set<Node, NodeHashFunction> d_refinement_lemma_vars;
+
/** adds lem as a refinement lemma */
void addRefinementLemma(Node lem);
/** add refinement lemma conjunct
@@ -175,7 +176,7 @@ class Cegis : public SygusModule
/** Get refinement evaluation lemmas
*
* This method performs "refinement evaluation", that is, it tests
- * whether the current solution, given by { candidates -> candidate_values },
+ * whether the current solution, given by { vs -> ms },
* satisfies all current refinement lemmas. If it does not, it may add
* blocking lemmas L to lems which exclude (a generalization of) the current
* solution.
@@ -191,6 +192,17 @@ class Cegis : public SygusModule
const std::vector<Node>& ms,
std::vector<Node>& lems,
bool doGen);
+ /** Check refinement evaluation lemmas
+ *
+ * This method is similar to above, but does not perform any generalization
+ * techniques. It is used when we are using only fast enumerators for
+ * all functions-to-synthesize.
+ *
+ * Returns true if a refinement lemma is false for the solution
+ * { vs -> ms }.
+ */
+ bool checkRefinementEvalLemmas(const std::vector<Node>& vs,
+ const std::vector<Node>& ms);
/** sampler object for the option cegisSample()
*
* This samples points of the type of the inner variables of the synthesis
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index b7c3851af..fe0e99a4d 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -55,10 +55,11 @@ SynthConjecture::SynthConjecture(QuantifiersEngine* qe,
d_ceg_proc(new SynthConjectureProcess(qe)),
d_ceg_gc(new CegGrammarConstructor(qe, this)),
d_sygus_rconst(new SygusRepairConst(qe)),
- d_sygus_ccore(new CegisCoreConnective(qe, this)),
+ d_exampleInfer(new ExampleInfer(d_tds)),
d_ceg_pbe(new SygusPbe(qe, this)),
d_ceg_cegis(new Cegis(qe, this)),
d_ceg_cegisUnif(new CegisUnif(qe, this)),
+ d_sygus_ccore(new CegisCoreConnective(qe, this)),
d_master(nullptr),
d_set_ce_sk_vars(false),
d_repair_index(0),
@@ -191,6 +192,15 @@ void SynthConjecture::assign(Node q)
}
}
}
+ // initialize the example inference utility
+ if (!d_exampleInfer->initialize(d_base_inst, d_candidates))
+ {
+ // there is a contradictory example pair, the conjecture is infeasible.
+ Node infLem = d_feasible_guard.negate();
+ d_qe->getOutputChannel().lemma(infLem);
+ // we don't need to continue initialization in this case
+ return;
+ }
// register this term with sygus database and other utilities that impact
// the enumerative sygus search
@@ -442,6 +452,16 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
Assert(candidate_values.empty());
constructed_cand = d_master->constructCandidates(
terms, enum_values, d_candidates, candidate_values, lems);
+ // now clear the evaluation caches
+ for (std::pair<const Node, std::unique_ptr<ExampleEvalCache> >& ecp :
+ d_exampleEvalCache)
+ {
+ ExampleEvalCache* eec = ecp.second.get();
+ if (eec != nullptr)
+ {
+ eec->clearEvaluationAll();
+ }
+ }
}
NodeManager* nm = NodeManager::currentNM();
@@ -1320,6 +1340,25 @@ Node SynthConjecture::getSymmetryBreakingPredicate(
}
}
+ExampleEvalCache* SynthConjecture::getExampleEvalCache(Node e)
+{
+ std::map<Node, std::unique_ptr<ExampleEvalCache> >::iterator it =
+ d_exampleEvalCache.find(e);
+ if (it != d_exampleEvalCache.end())
+ {
+ return it->second.get();
+ }
+ Node f = d_tds->getSynthFunForEnumerator(e);
+ // if f does not have examples, we don't construct the utility
+ if (!d_exampleInfer->hasExamples(f) || d_exampleInfer->getNumExamples(f) == 0)
+ {
+ d_exampleEvalCache[e].reset(nullptr);
+ return nullptr;
+ }
+ d_exampleEvalCache[e].reset(new ExampleEvalCache(d_tds, this, f, e));
+ return d_exampleEvalCache[e].get();
+}
+
} // namespace quantifiers
} // namespace theory
} /* namespace CVC4 */
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h
index a001572c2..a4f4af2e8 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.h
+++ b/src/theory/quantifiers/sygus/synth_conjecture.h
@@ -26,6 +26,8 @@
#include "theory/quantifiers/sygus/cegis.h"
#include "theory/quantifiers/sygus/cegis_core_connective.h"
#include "theory/quantifiers/sygus/cegis_unif.h"
+#include "theory/quantifiers/sygus/example_eval_cache.h"
+#include "theory/quantifiers/sygus/example_infer.h"
#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
#include "theory/quantifiers/sygus/sygus_pbe.h"
#include "theory/quantifiers/sygus/sygus_process_conj.h"
@@ -37,6 +39,7 @@ namespace theory {
namespace quantifiers {
class SynthEngine;
+class SygusStatistics;
/**
* A base class for generating values for actively-generated enumerators.
@@ -155,6 +158,10 @@ class SynthConjecture
SynthConjectureProcess* getProcess() { return d_ceg_proc.get(); }
/** get constant repair utility */
SygusRepairConst* getRepairConst() { return d_sygus_rconst.get(); }
+ /** get example inference utility */
+ ExampleInfer* getExampleInfer() { return d_exampleInfer.get(); }
+ /** get the example evaluation cache utility for enumerator e */
+ ExampleEvalCache* getExampleEvalCache(Node e);
/** get program by examples module */
SygusPbe* getPbe() { return d_ceg_pbe.get(); }
/** get the symmetry breaking predicate for type */
@@ -196,8 +203,10 @@ class SynthConjecture
std::unique_ptr<CegGrammarConstructor> d_ceg_gc;
/** repair constant utility */
std::unique_ptr<SygusRepairConst> d_sygus_rconst;
- /** connective core utility */
- std::unique_ptr<CegisCoreConnective> d_sygus_ccore;
+ /** example inference utility */
+ std::unique_ptr<ExampleInfer> d_exampleInfer;
+ /** example evaluation cache utility for each enumerator */
+ std::map<Node, std::unique_ptr<ExampleEvalCache> > d_exampleEvalCache;
//------------------------modules
/** program by examples module */
@@ -206,6 +215,8 @@ class SynthConjecture
std::unique_ptr<Cegis> d_ceg_cegis;
/** CEGIS UNIF module */
std::unique_ptr<CegisUnif> d_ceg_cegisUnif;
+ /** connective core utility */
+ std::unique_ptr<CegisCoreConnective> d_sygus_ccore;
/** the set of active modules (subset of the above list) */
std::vector<SygusModule*> d_modules;
/** master module
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback