src/theory/quantifiers/sygus/synth_conjecture.h

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