src/theory/quantifiers/sygus/synth_conjecture.h

   1 /*********************                                                        */
   2 /*! \file synth_conjecture.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Mathias Preiner, Haniel Barbosa
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Class that encapsulates techniques for a single (SyGuS) synthesis
  13  ** conjecture.
  14  **/
  15
  16 #include "cvc4_private.h"
  17
  18 #ifndef CVC4__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H
  19 #define CVC4__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H
  20
  21 #include <memory>
  22
  23 #include "theory/decision_manager.h"
  24 #include "theory/quantifiers/expr_miner_manager.h"
  25 #include "theory/quantifiers/sygus/ce_guided_single_inv.h"
  26 #include "theory/quantifiers/sygus/cegis.h"
  27 #include "theory/quantifiers/sygus/cegis_core_connective.h"
  28 #include "theory/quantifiers/sygus/cegis_unif.h"
  29 #include "theory/quantifiers/sygus/example_eval_cache.h"
  30 #include "theory/quantifiers/sygus/example_infer.h"
  31 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
  32 #include "theory/quantifiers/sygus/sygus_pbe.h"
  33 #include "theory/quantifiers/sygus/sygus_process_conj.h"
  34 #include "theory/quantifiers/sygus/sygus_repair_const.h"
  35 #include "theory/quantifiers/sygus/sygus_stats.h"
  36
  37 namespace CVC4 {
  38 namespace theory {
  39 namespace quantifiers {
  40
  41 class SynthEngine;
  42 class SygusStatistics;
  43
  44 /**
  45  * A base class for generating values for actively-generated enumerators.
  46  * At a high level, the job of this class is to accept a stream of "abstract
  47  * values" a1, ..., an, ..., and generate a (possibly larger) stream of
  48  * "concrete values" c11, ..., c1{m_1}, ..., cn1, ... cn{m_n}, ....
  49  */
  50 class EnumValGenerator
  51 {
  52  public:
  53   virtual ~EnumValGenerator() {}
  54   /** initialize this class with enumerator e */
  55   virtual void initialize(Node e) = 0;
  56   /** Inform this generator that abstract value v was enumerated. */
  57   virtual void addValue(Node v) = 0;
  58   /**
  59    * Increment this value generator. If this returns false, then we are out of
  60    * values. If this returns true, getCurrent(), if non-null, returns the
  61    * current term.
  62    *
  63    * Notice that increment() may return true and afterwards it may be the case
  64    * getCurrent() is null. We do this so that increment() does not take too
  65    * much time per call, which can be the case for grammars where it is
  66    * difficult to find the next (non-redundant) term. Returning true with
  67    * a null current term gives the caller the chance to interleave other
  68    * reasoning.
  69    */
  70   virtual bool increment() = 0;
  71   /** Get the current concrete value generated by this class. */
  72   virtual Node getCurrent() = 0;
  73 };
  74
  75 /** a synthesis conjecture
  76  * This class implements approaches for a synthesis conjecture, given by data
  77  * member d_quant.
  78  * This includes both approaches for synthesis in Reynolds et al CAV 2015. It
  79  * determines which approach and optimizations are applicable to the
  80  * conjecture, and has interfaces for implementing them.
  81  */
  82 class SynthConjecture
  83 {
  84  public:
  85   SynthConjecture(QuantifiersEngine* qe, SynthEngine* p, SygusStatistics& s);
  86   ~SynthConjecture();
  87   /** presolve */
  88   void presolve();
  89   /** get original version of conjecture */
  90   Node getConjecture() const { return d_quant; }
  91   /** get deep embedding version of conjecture */
  92   Node getEmbeddedConjecture() const { return d_embed_quant; }
  93   //-------------------------------for counterexample-guided check/refine
  94   /** whether the conjecture is waiting for a call to doCheck below */
  95   bool needsCheck();
  96   /** whether the conjecture is waiting for a call to doRefine below */
  97   bool needsRefinement() const;
  98   /** do syntax-guided enumerative check
  99    *
 100    * This is step 2(a) of Figure 3 of Reynolds et al CAV 2015.
 101    *
 102    * The method returns true if this conjecture is finished trying solutions
 103    * for the given call to SynthEngine::check.
 104    *
 105    * Notice that we make multiple calls to doCheck on one call to
 106    * SynthEngine::check. For example, if we are using an actively-generated
 107    * enumerator, one enumerated (abstract) term may correspond to multiple
 108    * concrete terms t1, ..., tn to check, where we make up to n calls to doCheck
 109    * when each of t1, ..., tn fails to satisfy the current refinement lemmas.
 110    */
 111   bool doCheck(std::vector<Node>& lems);
 112   /** do refinement
 113    *
 114    * This is step 2(b) of Figure 3 of Reynolds et al CAV 2015.
 115    *
 116    * This method is run when needsRefinement() returns true, indicating that
 117    * the last call to doCheck found a counterexample to the last candidate.
 118    *
 119    * This method adds a refinement lemma on the output channel of quantifiers
 120    * engine. If the refinement lemma is a duplicate, then we manually
 121    * exclude the current candidate via excludeCurrentSolution. This should
 122    * only occur when the synthesis conjecture for the current candidate fails
 123    * to evaluate to false for a given counterexample point, but regardless its
 124    * negation is satisfiable for the current candidate and that point. This is
 125    * exclusive to theories with partial functions, e.g. (non-linear) division.
 126    *
 127    * This method returns true if a lemma was added on the output channel, and
 128    * false otherwise.
 129    */
 130   bool doRefine();
 131   //-------------------------------end for counterexample-guided check/refine
 132   /**
 133    * Prints the synthesis solution to output stream out. This invokes solution
 134    * reconstruction if the conjecture is single invocation. Otherwise, it
 135    * returns the solution found by sygus enumeration.
 136    */
 137   void printSynthSolution(std::ostream& out);
 138   /** get synth solutions
 139    *
 140    * This method returns true if this class has a solution available to the
 141    * conjecture that it was assigned.
 142    *
 143    * Let q be the synthesis conjecture assigned to this class.
 144    * This method adds entries to sol_map[q] that map functions-to-synthesize to
 145    * their builtin solution, which has the same type. For example, for synthesis
 146    * conjecture exists f. forall x. f( x )>x, this function will update
 147    * sol_map[q] to contain the entry:
 148    *   f -> (lambda x. x+1)
 149    */
 150   bool getSynthSolutions(std::map<Node, std::map<Node, Node> >& sol_map);
 151   /**
 152    * The feasible guard whose semantics are "this conjecture is feasiable".
 153    * This is "G" in Figure 3 of Reynolds et al CAV 2015.
 154    */
 155   Node getGuard() const;
 156   /** is ground */
 157   bool isGround() { return d_inner_vars.empty(); }
 158   /** are we using single invocation techniques */
 159   bool isSingleInvocation() const;
 160   /** preregister conjecture
 161    * This is used as a heuristic for solution reconstruction, so that we
 162    * remember expressions in the conjecture before preprocessing, since they
 163    * may be helpful during solution reconstruction (Figure 5 of Reynolds et al
 164    * CAV 2015)
 165    */
 166   void preregisterConjecture(Node q);
 167   /** assign conjecture q to this class */
 168   void assign(Node q);
 169   /** has a conjecture been assigned to this class */
 170   bool isAssigned() { return !d_embed_quant.isNull(); }
 171   /**
 172    * Get model value for term n.
 173    */
 174   Node getModelValue(Node n);
 175
 176   /** get utility for static preprocessing and analysis of conjectures */
 177   SynthConjectureProcess* getProcess() { return d_ceg_proc.get(); }
 178   /** get constant repair utility */
 179   SygusRepairConst* getRepairConst() { return d_sygus_rconst.get(); }
 180   /** get example inference utility */
 181   ExampleInfer* getExampleInfer() { return d_exampleInfer.get(); }
 182   /** get the example evaluation cache utility for enumerator e */
 183   ExampleEvalCache* getExampleEvalCache(Node e);
 184   /** get program by examples module */
 185   SygusPbe* getPbe() { return d_ceg_pbe.get(); }
 186   /** get the symmetry breaking predicate for type */
 187   Node getSymmetryBreakingPredicate(
 188       Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth);
 189   /** print out debug information about this conjecture */
 190   void debugPrint(const char* c);
 191   /** check side condition
 192    *
 193    * This returns false if the solution { d_candidates -> cvals } does not
 194    * satisfy the side condition of the conjecture maintained by this class,
 195    * if it exists, and true otherwise.
 196    */
 197   bool checkSideCondition(const std::vector<Node>& cvals) const;
 198
 199  private:
 200   /** reference to quantifier engine */
 201   QuantifiersEngine* d_qe;
 202   /** pointer to the synth engine that owns this */
 203   SynthEngine* d_parent;
 204   /** reference to the statistics of parent */
 205   SygusStatistics& d_stats;
 206   /** term database sygus of d_qe */
 207   TermDbSygus* d_tds;
 208   /** The feasible guard. */
 209   Node d_feasible_guard;
 210   /**
 211    * Do we have a solution in this solve context? This flag is reset to false
 212    * on every call to presolve.
 213    */
 214   bool d_hasSolution;
 215   /** the decision strategy for the feasible guard */
 216   std::unique_ptr<DecisionStrategy> d_feasible_strategy;
 217   /** single invocation utility */
 218   std::unique_ptr<CegSingleInv> d_ceg_si;
 219   /** utility for static preprocessing and analysis of conjectures */
 220   std::unique_ptr<SynthConjectureProcess> d_ceg_proc;
 221   /** grammar utility */
 222   std::unique_ptr<CegGrammarConstructor> d_ceg_gc;
 223   /** repair constant utility */
 224   std::unique_ptr<SygusRepairConst> d_sygus_rconst;
 225   /** example inference utility */
 226   std::unique_ptr<ExampleInfer> d_exampleInfer;
 227   /** example evaluation cache utility for each enumerator */
 228   std::map<Node, std::unique_ptr<ExampleEvalCache> > d_exampleEvalCache;
 229
 230   //------------------------modules
 231   /** program by examples module */
 232   std::unique_ptr<SygusPbe> d_ceg_pbe;
 233   /** CEGIS module */
 234   std::unique_ptr<Cegis> d_ceg_cegis;
 235   /** CEGIS UNIF module */
 236   std::unique_ptr<CegisUnif> d_ceg_cegisUnif;
 237   /** connective core utility */
 238   std::unique_ptr<CegisCoreConnective> d_sygus_ccore;
 239   /** the set of active modules (subset of the above list) */
 240   std::vector<SygusModule*> d_modules;
 241   /** master module
 242    *
 243    * This is the module (one of those above) that takes sole responsibility
 244    * for this conjecture, determined during assign(...).
 245    */
 246   SygusModule* d_master;
 247   //------------------------end modules
 248
 249   //------------------------enumerators
 250   /**
 251    * Get model values for terms n, store in vector v. This method returns true
 252    * if and only if all values added to v are non-null.
 253    *
 254    * The argument activeIncomplete indicates whether n contains an active
 255    * enumerator that is currently not finished enumerating values, but returned
 256    * null on a call to getEnumeratedValue. This value is used for determining
 257    * whether we should call getEnumeratedValues again within a call to
 258    * SynthConjecture::check.
 259    *
 260    * It removes terms from n that correspond to "inactive" enumerators, that
 261    * is, enumerators whose values have been exhausted.
 262    */
 263   bool getEnumeratedValues(std::vector<Node>& n,
 264                            std::vector<Node>& v,
 265                            bool& activeIncomplete);
 266   /**
 267    * Get model value for term n. If n has a value that was excluded by
 268    * datatypes sygus symmetry breaking, this method returns null. It sets
 269    * activeIncomplete to true if there is an actively-generated enumerator whose
 270    * current value is null but it has not finished generating values.
 271    */
 272   Node getEnumeratedValue(Node n, bool& activeIncomplete);
 273   /** enumerator generators for each actively-generated enumerator */
 274   std::map<Node, std::unique_ptr<EnumValGenerator> > d_evg;
 275   /**
 276    * Map from enumerators to whether they are currently being
 277    * "actively-generated". That is, we are in a state where we have called
 278    * d_evg[e].addValue(v) for some v, and d_evg[e].getNext() has not yet
 279    * returned null. The range of this map stores the abstract value that
 280    * we are currently generating values from.
 281    */
 282   std::map<Node, Node> d_ev_curr_active_gen;
 283   /** the current waiting value of each actively-generated enumerator, if any
 284    *
 285    * This caches values that are actively generated and that we have not yet
 286    * passed to a call to SygusModule::constructCandidates. An example of when
 287    * this may occur is when there are two actively-generated enumerators e1 and
 288    * e2. Say on some iteration we actively-generate v1 for e1, the value
 289    * of e2 was excluded by symmetry breaking, and say the current master sygus
 290    * module does not handle partial models. Hence, we abort the current check.
 291    * We remember that the value of e1 was v1 by storing it here, so that on
 292    * a future check when v2 has a proper value, it is returned.
 293    */
 294   std::map<Node, Node> d_ev_active_gen_waiting;
 295   /** the first value enumerated for each actively-generated enumerator
 296    *
 297    * This is to implement an optimization that only guards the blocking lemma
 298    * for the first value of an actively-generated enumerator.
 299    */
 300   std::map<Node, Node> d_ev_active_gen_first_val;
 301   //------------------------end enumerators
 302
 303   /** list of constants for quantified formula
 304    * The outer Skolems for the negation of d_embed_quant.
 305    */
 306   std::vector<Node> d_candidates;
 307   /** base instantiation
 308    * If d_embed_quant is forall d. exists y. P( d, y ), then
 309    * this is the formula  exists y. P( d_candidates, y ). Notice that
 310    * (exists y. F) is shorthand above for ~( forall y. ~F ).
 311    */
 312   Node d_base_inst;
 313   /** list of variables on inner quantification */
 314   std::vector<Node> d_inner_vars;
 315   /**
 316    * The set of skolems for the current "verification" lemma, if one exists.
 317    * This may be added to during calls to doCheck(). The model values for these
 318    * skolems are analyzed during doRefine().
 319    */
 320   std::vector<Node> d_ce_sk_vars;
 321   /**
 322    * If we have already tested the satisfiability of the current verification
 323    * lemma, this stores the model values of d_ce_sk_vars in the current
 324    * (satisfiable, failed) verification lemma.
 325    */
 326   std::vector<Node> d_ce_sk_var_mvs;
 327   /**
 328    * Whether the above vector has been set. We have this flag since the above
 329    * vector may be set to empty (e.g. for ground synthesis conjectures).
 330    */
 331   bool d_set_ce_sk_vars;
 332
 333   /** the asserted (negated) conjecture */
 334   Node d_quant;
 335   /**
 336    * The side condition for solving the conjecture, after conversion to deep
 337    * embedding.
 338    */
 339   Node d_embedSideCondition;
 340   /** (negated) conjecture after simplification */
 341   Node d_simp_quant;
 342   /** (negated) conjecture after simplification, conversion to deep embedding */
 343   Node d_embed_quant;
 344   /** candidate information */
 345   class CandidateInfo
 346   {
 347    public:
 348     CandidateInfo() {}
 349     /** list of terms we have instantiated candidates with */
 350     std::vector<Node> d_inst;
 351   };
 352   std::map<Node, CandidateInfo> d_cinfo;
 353   /**
 354    * The first index of an instantiation in CandidateInfo::d_inst that we have
 355    * not yet tried to repair.
 356    */
 357   unsigned d_repair_index;
 358   /** number of times we have called doRefine */
 359   unsigned d_refine_count;
 360   /** get candidadate */
 361   Node getCandidate(unsigned int i) { return d_candidates[i]; }
 362   /** record instantiation (this is used to construct solutions later) */
 363   void recordInstantiation(std::vector<Node>& vs)
 364   {
 365     Assert(vs.size() == d_candidates.size());
 366     for (unsigned i = 0; i < vs.size(); i++)
 367     {
 368       d_cinfo[d_candidates[i]].d_inst.push_back(vs[i]);
 369     }
 370   }
 371   /** get synth solutions internal
 372    *
 373    * This function constructs the body of solutions for all
 374    * functions-to-synthesize in this conjecture and stores them in sols, in
 375    * order. For each solution added to sols, we add an integer indicating what
 376    * kind of solution n is, where if sols[i] = n, then
 377    *   if status[i] = 0: n is the (builtin term) corresponding to the solution,
 378    *   if status[i] = 1: n is the sygus representation of the solution.
 379    * We store builtin versions under some conditions (such as when the sygus
 380    * grammar is being ignored).
 381    *
 382    * This consults the single invocation module to get synthesis solutions if
 383    * isSingleInvocation() returns true.
 384    *
 385    * For example, for conjecture exists fg. forall x. f(x)>g(x), this function
 386    * may set ( sols, status ) to ( { x+1, d_x() }, { 1, 0 } ), where d_x() is
 387    * the sygus datatype constructor corresponding to variable x.
 388    */
 389   bool getSynthSolutionsInternal(std::vector<Node>& sols,
 390                                  std::vector<int>& status);
 391   //-------------------------------- sygus stream
 392   /** current stream guard */
 393   Node d_current_stream_guard;
 394   /** the decision strategy for streaming solutions */
 395   class SygusStreamDecisionStrategy : public DecisionStrategyFmf
 396   {
 397    public:
 398     SygusStreamDecisionStrategy(context::Context* satContext,
 399                                 Valuation valuation);
 400     /** make literal */
 401     Node mkLiteral(unsigned i) override;
 402     /** identify */
 403     std::string identify() const override
 404     {
 405       return std::string("sygus_stream");
 406     }
 407   };
 408   std::unique_ptr<SygusStreamDecisionStrategy> d_stream_strategy;
 409   /** get current stream guard */
 410   Node getCurrentStreamGuard() const;
 411   /** get stream guarded lemma
 412    *
 413    * If sygusStream is enabled, this returns ( G V n ) where G is the guard
 414    * returned by getCurrentStreamGuard, otherwise this returns n.
 415    */
 416   Node getStreamGuardedLemma(Node n) const;
 417   /**
 418    * Prints the current synthesis solution to the output stream indicated by
 419    * the Options object, send a lemma blocking the current solution to the
 420    * output channel, which we refer to as a "stream exclusion lemma".
 421    *
 422    * The argument enums is the set of enumerators that comprise the current
 423    * solution, and values is their current values.
 424    */
 425   void printAndContinueStream(const std::vector<Node>& enums,
 426                               const std::vector<Node>& values);
 427   /** exclude the current solution { enums -> values } */
 428   void excludeCurrentSolution(const std::vector<Node>& enums,
 429                               const std::vector<Node>& values);
 430   /**
 431    * Whether we have guarded a stream exclusion lemma when using sygusStream.
 432    * This is an optimization that allows us to guard only the first stream
 433    * exclusion lemma.
 434    */
 435   bool d_guarded_stream_exc;
 436   //-------------------------------- end sygus stream
 437   /** expression miner managers for each function-to-synthesize
 438    *
 439    * Notice that for each function-to-synthesize, we enumerate a stream of
 440    * candidate solutions, where each of these streams is independent. Thus,
 441    * we maintain separate expression miner managers for each of them.
 442    *
 443    * This is used for the sygusRewSynth() option to synthesize new candidate
 444    * rewrite rules.
 445    */
 446   std::map<Node, ExpressionMinerManager> d_exprm;
 447 };
 448
 449 }  // namespace quantifiers
 450 }  // namespace theory
 451 } /* namespace CVC4 */
 452
 453 #endif