src/theory/quantifiers/sygus/synth_conjecture.h

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