/*! \file synth_conjecture.h
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Haniel Barbosa, Tim King
+ ** Andrew Reynolds, Mathias Preiner, Haniel Barbosa
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
#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"
#include "theory/quantifiers/sygus/sygus_repair_const.h"
#include "theory/quantifiers/sygus/sygus_stats.h"
+#include "theory/quantifiers/sygus/template_infer.h"
namespace CVC4 {
namespace theory {
namespace quantifiers {
-class SynthEngine;
+class SygusStatistics;
/**
* A base class for generating values for actively-generated enumerators.
* Increment this value generator. If this returns false, then we are out of
* values. If this returns true, getCurrent(), if non-null, returns the
* current term.
+ *
+ * Notice that increment() may return true and afterwards it may be the case
+ * getCurrent() is null. We do this so that increment() does not take too
+ * much time per call, which can be the case for grammars where it is
+ * difficult to find the next (non-redundant) term. Returning true with
+ * a null current term gives the caller the chance to interleave other
+ * reasoning.
*/
virtual bool increment() = 0;
/** Get the current concrete value generated by this class. */
};
/** a synthesis conjecture
- * This class implements approaches for a synthesis conecjture, given by data
+ * This class implements approaches for a synthesis conjecture, given by data
* member d_quant.
* This includes both approaches for synthesis in Reynolds et al CAV 2015. It
* determines which approach and optimizations are applicable to the
class SynthConjecture
{
public:
- SynthConjecture(QuantifiersEngine* qe, SynthEngine* p, SygusStatistics& s);
+ SynthConjecture(QuantifiersEngine* qe,
+ QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
+ SygusStatistics& s);
~SynthConjecture();
/** presolve */
void presolve();
/** get original version of conjecture */
- Node getConjecture() { return d_quant; }
+ Node getConjecture() const { return d_quant; }
/** get deep embedding version of conjecture */
- Node getEmbeddedConjecture() { return d_embed_quant; }
+ Node getEmbeddedConjecture() const { return d_embed_quant; }
//-------------------------------for counterexample-guided check/refine
- /** increment the number of times we have successfully done candidate
- * refinement */
- void incrementRefineCount() { d_refine_count++; }
/** whether the conjecture is waiting for a call to doCheck below */
bool needsCheck();
/** whether the conjecture is waiting for a call to doRefine below */
*/
bool doCheck(std::vector<Node>& lems);
/** do refinement
+ *
* This is step 2(b) of Figure 3 of Reynolds et al CAV 2015.
+ *
+ * This method is run when needsRefinement() returns true, indicating that
+ * the last call to doCheck found a counterexample to the last candidate.
+ *
+ * This method adds a refinement lemma on the output channel of quantifiers
+ * engine. If the refinement lemma is a duplicate, then we manually
+ * exclude the current candidate via excludeCurrentSolution. This should
+ * only occur when the synthesis conjecture for the current candidate fails
+ * to evaluate to false for a given counterexample point, but regardless its
+ * negation is satisfiable for the current candidate and that point. This is
+ * exclusive to theories with partial functions, e.g. (non-linear) division.
+ *
+ * This method returns true if a lemma was added on the output channel, and
+ * false otherwise.
*/
- void doRefine(std::vector<Node>& lems);
+ bool doRefine();
//-------------------------------end for counterexample-guided check/refine
/**
* Prints the synthesis solution to output stream out. This invokes solution
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 */
private:
/** reference to quantifier engine */
QuantifiersEngine* d_qe;
- /** pointer to the synth engine that owns this */
- SynthEngine* d_parent;
+ /** Reference to the quantifiers state */
+ QuantifiersState& d_qstate;
+ /** Reference to the quantifiers inference manager */
+ QuantifiersInferenceManager& d_qim;
/** reference to the statistics of parent */
SygusStatistics& d_stats;
/** term database sygus of d_qe */
std::unique_ptr<DecisionStrategy> d_feasible_strategy;
/** single invocation utility */
std::unique_ptr<CegSingleInv> d_ceg_si;
+ /** template inference utility */
+ std::unique_ptr<SygusTemplateInfer> d_templInfer;
/** utility for static preprocessing and analysis of conjectures */
std::unique_ptr<SynthConjectureProcess> d_ceg_proc;
/** grammar utility */
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 */
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
unsigned d_repair_index;
/** number of times we have called doRefine */
unsigned d_refine_count;
- /** get candidadate */
- Node getCandidate(unsigned int i) { return d_candidates[i]; }
- /** record instantiation (this is used to construct solutions later) */
- void recordInstantiation(std::vector<Node>& vs)
- {
- Assert(vs.size() == d_candidates.size());
- for (unsigned i = 0; i < vs.size(); i++)
- {
- d_cinfo[d_candidates[i]].d_inst.push_back(vs[i]);
- }
- }
+ /** record solution (this is used to construct solutions later) */
+ void recordSolution(std::vector<Node>& vs);
/** get synth solutions internal
*
* This function constructs the body of solutions for all
bool getSynthSolutionsInternal(std::vector<Node>& sols,
std::vector<int>& status);
//-------------------------------- sygus stream
- /** current stream guard */
- Node d_current_stream_guard;
- /** the decision strategy for streaming solutions */
- class SygusStreamDecisionStrategy : public DecisionStrategyFmf
- {
- public:
- SygusStreamDecisionStrategy(context::Context* satContext,
- Valuation valuation);
- /** make literal */
- Node mkLiteral(unsigned i) override;
- /** identify */
- std::string identify() const override
- {
- return std::string("sygus_stream");
- }
- };
- std::unique_ptr<SygusStreamDecisionStrategy> d_stream_strategy;
- /** get current stream guard */
- Node getCurrentStreamGuard() const;
- /** get stream guarded lemma
- *
- * If sygusStream is enabled, this returns ( G V n ) where G is the guard
- * returned by getCurrentStreamGuard, otherwise this returns n.
- */
- Node getStreamGuardedLemma(Node n) const;
/**
* Prints the current synthesis solution to the output stream indicated by
* the Options object, send a lemma blocking the current solution to the
projects / cvc5.git / blobdiff