src/theory/quantifiers/sygus/sygus_invariance.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds, Mathias Preiner, Tim King
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 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.
  11  * ****************************************************************************
  12  *
  13  * Sygus invariance tests.
  14  */
  15
  16 #include "cvc5_private.h"
  17
  18 #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H
  19 #define CVC5__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H
  20
  21 #include <unordered_map>
  22 #include <vector>
  23
  24 #include "expr/node.h"
  25
  26 namespace cvc5 {
  27 namespace theory {
  28 namespace quantifiers {
  29
  30 class TermDbSygus;
  31 class SynthConjecture;
  32
  33 /* SygusInvarianceTest
  34 *
  35 * This class is the standard interface for term generalization
  36 * in SyGuS. Its interface is a single function is_variant,
  37 * which is a virtual condition for SyGuS terms.
  38 *
  39 * The common use case of invariance tests is when constructing
  40 * minimal explanations for refinement lemmas in the
  41 * counterexample-guided inductive synthesis (CEGIS) loop.
  42 * See sygus_explain.h for more details.
  43 */
  44 class SygusInvarianceTest
  45 {
  46  public:
  47   virtual ~SygusInvarianceTest() {}
  48
  49   /** Is nvn invariant with respect to this test ?
  50    *
  51    * - nvn is the term to check whether it is invariant.
  52    * - x is a variable such that the previous call to
  53    *   is_invariant (if any) was with term nvn_prev, and
  54    *   nvn is equal to nvn_prev with some subterm
  55    *   position replaced by x. This is typically used
  56    *   for debugging only.
  57    */
  58   bool is_invariant(TermDbSygus* tds, Node nvn, Node x)
  59   {
  60     if (invariant(tds, nvn, x))
  61     {
  62       d_update_nvn = nvn;
  63       return true;
  64     }
  65     return false;
  66   }
  67   /** get updated term */
  68   Node getUpdatedTerm() { return d_update_nvn; }
  69   /** set updated term */
  70   void setUpdatedTerm(Node n) { d_update_nvn = n; }
  71  protected:
  72   /** result of the node that satisfies this invariant */
  73   Node d_update_nvn;
  74   /** check whether nvn[ x ] is invariant */
  75   virtual bool invariant(TermDbSygus* tds, Node nvn, Node x) = 0;
  76 };
  77
  78 /** EquivSygusInvarianceTest
  79 *
  80 * This class tests whether a term evaluates via evaluation
  81 * operators in the deep embedding (Section 4 of Reynolds
  82 * et al. CAV 2015) to fixed term d_result.
  83 *
  84 * For example, consider a SyGuS evaluation function eval
  85 * for a synthesis conjecture with arguments x and y.
  86 * Notice that the term t = (mult x y) is such that:
  87 *   eval( t, 0, 1 ) ----> 0
  88 * This test is invariant on the content of the second
  89 * argument of t, noting that:
  90 *   eval( (mult x _), 0, 1 ) ----> 0
  91 * as well, via a call to EvalSygusInvarianceTest::invariant.
  92 *
  93 * Another example, t = ite( gt( x, y ), x, y ) is such that:
  94 *   eval( t, 2, 3 ) ----> 3
  95 * This test is invariant on the second child of t, noting:
  96 *   eval( ite( gt( x, y ), _, y ), 2, 3 ) ----> 3
  97 */
  98 class EvalSygusInvarianceTest : public SygusInvarianceTest
  99 {
 100  public:
 101   EvalSygusInvarianceTest()
 102       : d_kind(kind::UNDEFINED_KIND), d_is_conjunctive(false)
 103   {
 104   }
 105
 106   /** initialize this invariance test
 107    *
 108    * This sets d_terms/d_var/d_result, where we are checking whether:
 109    *   <d_kind>(d_terms) { d_var -> n } ----> d_result.
 110    * for terms n.
 111    */
 112   void init(Node conj, Node var, Node res);
 113
 114  protected:
 115   /** does d_terms{ d_var -> nvn } still rewrite to d_result? */
 116   bool invariant(TermDbSygus* tds, Node nvn, Node x) override;
 117
 118  private:
 119   /** the formulas we are evaluating */
 120   std::vector<Node> d_terms;
 121   /** the variable */
 122   TNode d_var;
 123   /** the result of the evaluation */
 124   Node d_result;
 125   /** the parent kind we are checking, undefined if size(d_terms) is 1. */
 126   Kind d_kind;
 127   /** whether we are conjunctive
 128    *
 129    * If this flag is true, then the evaluation tests:
 130    *   d_terms[1] {d_var -> n} = d_result ... d_term[k] {d_var -> n} = d_result
 131    * should be processed conjunctively, that is,
 132    * <d_kind>(d_terms) { d_var -> n } = d_result only if each of the above
 133    * holds. If this flag is false, then these tests are interpreted
 134    * disjunctively, i.e. if one child test succeeds, the overall test succeeds.
 135    */
 136   bool d_is_conjunctive;
 137 };
 138
 139 /** EquivSygusInvarianceTest
 140 *
 141 * This class tests whether a builtin version of a
 142 * sygus term is equivalent up to rewriting to a RHS value bvr.
 143 *
 144 * For example,
 145 *
 146 * ite( t>0, 0, 0 ) + s*0 ----> 0
 147 *
 148 * This test is invariant on the condition t>0 and s, since:
 149 *
 150 * ite( _, 0, 0 ) + _*0 ----> 0
 151 *
 152 * for any values of _.
 153 *
 154 * It also manages the case where the rewriting is invariant
 155 * wrt a finite set of examples occurring in the conjecture.
 156 * (EX1) : For example if our input examples are:
 157 * (x,y,z) = (3,2,4), (5,2,6), (3,2,1)
 158 * On these examples, we have:
 159 *
 160 * ite( x>y, z, 0) ---> 4,6,1
 161 *
 162 * which is invariant on the second argument:
 163 *
 164 * ite( x>y, z, _) ---> 4,6,1
 165 *
 166 * For details, see Reynolds et al SYNT 2017.
 167 */
 168 class EquivSygusInvarianceTest : public SygusInvarianceTest
 169 {
 170  public:
 171   EquivSygusInvarianceTest() : d_conj(nullptr) {}
 172
 173   /** initialize this invariance test
 174    * tn is the sygus type for e
 175    * aconj/e are used for conjecture-specific symmetry breaking
 176    * bvr is the builtin version of the right hand side of the rewrite that we
 177    * are checking for invariance
 178    */
 179   void init(
 180       TermDbSygus* tds, TypeNode tn, SynthConjecture* aconj, Node e, Node bvr);
 181
 182  protected:
 183   /** checks whether the analog of nvn still rewrites to d_bvr */
 184   bool invariant(TermDbSygus* tds, Node nvn, Node x) override;
 185
 186  private:
 187   /** the conjecture associated with the enumerator d_enum */
 188   SynthConjecture* d_conj;
 189   /** the enumerator associated with the term for which this test is for */
 190   Node d_enum;
 191   /** the RHS of the evaluation */
 192   Node d_bvr;
 193   /** the result of the examples
 194    * In (EX1), this is (4,6,1)
 195    */
 196   std::vector<Node> d_exo;
 197 };
 198
 199 /** DivByZeroSygusInvarianceTest
 200  *
 201  * This class tests whether a sygus term involves
 202  * division by zero.
 203  *
 204  * For example the test for:
 205  *    ( x + ( y/0 )*2 )
 206  * is invariant on the contents of _ below:
 207  *    ( _ + ( _/0 )*_ )
 208  */
 209 class DivByZeroSygusInvarianceTest : public SygusInvarianceTest
 210 {
 211  public:
 212   DivByZeroSygusInvarianceTest() {}
 213
 214  protected:
 215   /** checks whether nvn involves division by zero. */
 216   bool invariant(TermDbSygus* tds, Node nvn, Node x) override;
 217 };
 218
 219 /** NegContainsSygusInvarianceTest
 220 *
 221 * This class is used to construct a minimal shape of a term that cannot
 222 * be contained in at least one output of an I/O pair.
 223 *
 224 * Say our PBE conjecture is:
 225 *
 226 * exists f.
 227 *   f( "abc" ) = "abc abc" ^
 228 *   f( "de" ) = "de de"
 229 *
 230 * Then, this class is used when there is a candidate solution t[x1]
 231 * such that either:
 232 *   contains( "abc abc", t["abc"] ) ---> false or
 233 *   contains( "de de", t["de"] ) ---> false
 234 *
 235 * It is used to determine whether certain generalizations of t[x1]
 236 * are still sufficient to falsify one of the above containments.
 237 *
 238 * For example:
 239 *
 240 * The test for str.++( x1, "d" ) is invariant on its first argument
 241 *   ...since contains( "abc abc", str.++( _, "d" ) ) ---> false
 242 * The test for str.replace( "de", x1, "b" ) is invariant on its third argument
 243 *   ...since contains( "abc abc", str.replace( "de", "abc", _ ) ) ---> false
 244 */
 245 class NegContainsSygusInvarianceTest : public SygusInvarianceTest
 246 {
 247  public:
 248   NegContainsSygusInvarianceTest() : d_isUniversal(false) {}
 249
 250   /** initialize this invariance test
 251    *  e is the enumerator which we are reasoning about (associated with a synth
 252    *    fun).
 253    *  ex is the list of inputs,
 254    *  exo is the list of outputs,
 255    *  ncind is the set of possible example indices to check invariance of
 256    *  non-containment.
 257    *    For example, in the above example, when t[x1] = "ab", then this
 258    *    has the index 1 since contains("de de", "ab") ---> false but not
 259    *    the index 0 since contains("abc abc","ab") ---> true.
 260    */
 261   void init(Node e,
 262             std::vector<std::vector<Node> >& ex,
 263             std::vector<Node>& exo,
 264             std::vector<unsigned>& ncind);
 265   /** set universal
 266    *
 267    * This updates the semantics of this check such that *all* instead of some
 268    * examples must fail the containment test.
 269    */
 270   void setUniversal() { d_isUniversal = true; }
 271
 272  protected:
 273   /**
 274    * Checks if contains( out_i, nvn[in_i] ) --> false for some I/O pair i; if
 275    * d_isUniversal is true, then we check if the rewrite holds for *all* I/O
 276    * pairs.
 277    */
 278   bool invariant(TermDbSygus* tds, Node nvn, Node x) override;
 279
 280  private:
 281   /** The enumerator whose value we are considering in this invariance test */
 282   Node d_enum;
 283   /** The input examples */
 284   std::vector<std::vector<Node> > d_ex;
 285   /** The output examples for the enumerator */
 286   std::vector<Node> d_exo;
 287   /** The set of I/O pair indices i such that
 288    *    contains( out_i, nvn[in_i] ) ---> false
 289    */
 290   std::vector<unsigned> d_neg_con_indices;
 291   /** requires not being in all examples */
 292   bool d_isUniversal;
 293 };
 294
 295 }  // namespace quantifiers
 296 }  // namespace theory
 297 }  // namespace cvc5
 298
 299 #endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H */