Unified fairness scheme for cegis unif (#1941)

8 files changed, 674 insertions, 23 deletions

diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 692055b87..57c4c1ad3 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -330,11 +330,23 @@ void CegisUnifEnumManager::getEnumeratorsForStrategyPt(Node e,
                                                        std::vector<Node>& es,
                                                        unsigned index) const
 {
-  std::map<Node, StrategyPtInfo>::const_iterator itc = d_ce_info.find(e);
-  Assert(itc != d_ce_info.end());
-  es.insert(es.end(),
-            itc->second.d_enums[index].begin(),
-            itc->second.d_enums[index].end());
+  // the number of active enumerators is related to the current cost value
+  unsigned num_enums = d_curr_guq_val.get();
+  Assert(num_enums > 0);
+  if (index == 1)
+  {
+    // we always use (cost-1) conditions
+    num_enums = num_enums - 1;
+  }
+  if (num_enums > 0)
+  {
+    std::map<Node, StrategyPtInfo>::const_iterator itc = d_ce_info.find(e);
+    Assert(itc != d_ce_info.end());
+    Assert(num_enums <= itc->second.d_enums[index].size());
+    es.insert(es.end(),
+              itc->second.d_enums[index].begin(),
+              itc->second.d_enums[index].begin() + num_enums);
+  }
 }
 
 void CegisUnifEnumManager::registerEvalPts(const std::vector<Node>& eis, Node e)
@@ -469,6 +481,57 @@ void CegisUnifEnumManager::incrementNumEnumerators()
         registerEvalPtAtSize(c, ei, new_lit, new_size);
       }
     }
+    // enforce fairness between number of enumerators and enumerator size
+    if (new_size > 1)
+    {
+      // construct the "virtual enumerator"
+      if (d_virtual_enum.isNull())
+      {
+        // we construct the default integer grammar with no variables, e.g.:
+        //   A -> 0 | 1 | A+A
+        TypeNode intTn = nm->integerType();
+        // use a null variable list
+        Node bvl;
+        std::stringstream ss;
+        ss << "_virtual_enum_grammar";
+        std::string virtualEnumName(ss.str());
+        std::map<TypeNode, std::vector<Node>> extra_cons;
+        std::map<TypeNode, std::vector<Node>> exclude_cons;
+        // do not include "-", which is included by default for integers
+        exclude_cons[intTn].push_back(nm->operatorOf(MINUS));
+        std::unordered_set<Node, NodeHashFunction> term_irrelevant;
+        TypeNode vtn =
+            CegGrammarConstructor::mkSygusDefaultType(intTn,
+                                                      bvl,
+                                                      virtualEnumName,
+                                                      extra_cons,
+                                                      exclude_cons,
+                                                      term_irrelevant);
+        d_virtual_enum = nm->mkSkolem("_ve", vtn);
+        d_tds->registerEnumerator(d_virtual_enum, Node::null(), d_parent);
+      }
+      // if new_size is a power of two, then isPow2 returns log2(new_size)+1
+      // otherwise, this returns 0. In the case it returns 0, we don't care
+      // since the floor( log2( i ) ) = floor( log2( i - 1 ) ) and we do not
+      // increase our size bound.
+      unsigned pow_two = Integer(new_size).isPow2();
+      if (pow_two > 0)
+      {
+        Node size_ve = nm->mkNode(DT_SIZE, d_virtual_enum);
+        Node fair_lemma =
+            nm->mkNode(GEQ, size_ve, nm->mkConst(Rational(pow_two - 1)));
+        fair_lemma = nm->mkNode(OR, new_lit, fair_lemma);
+        Trace("cegis-unif-enum-lemma")
+            << "CegisUnifEnum::lemma, fairness size:" << fair_lemma << "\n";
+        // this lemma relates the number of conditions we enumerate and the
+        // maximum size of a term that is part of our solution. It is of the
+        // form:
+        //   G_uq_i => size(ve) >= log_2( i-1 )
+        // In other words, if we use i conditions, then we allow terms in our
+        // solution whose size is at most log_2(i-1).
+        d_qe->getOutputChannel().lemma(fair_lemma);
+      }
+    }
   }
 }
 
diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h
index 5c2c11e4d..80c11f82d 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -142,6 +142,24 @@ class CegisUnifEnumManager
   std::map<unsigned, Node> d_guq_lit;
   /** Have we returned a decision in the current SAT context? */
   context::CDO<bool> d_ret_dec;
+  /** the "virtual" enumerator
+   *
+   * This enumerator is used for enforcing fairness. In particular, we relate
+   * its size to the number of conditions allocated by this class such that:
+   *    ~G_uq_i => size(d_virtual_enum) >= floor( log2( i-1 ) )
+   * In other words, if we are using (i-1) conditions in our solution,
+   * the size of the virtual enumerator is at least the floor of the log (base
+   * two) of (i-1). Due to the default fairness scheme in the quantifier-free
+   * datatypes solver (if --sygus-fair-max is enabled), this ensures that other
+   * enumerators are allowed to have at least this size. This affect other
+   * fairness schemes in an analogous fashion. In particular, we enumerate
+   * based on the tuples for (term size, #conditions):
+   *   (0,0), (0,1)                                             [size 0]
+   *   (0,2), (0,3), (1,1), (1,2), (1,3)                        [size 1]
+   *   (0,4), ..., (0,7), (1,4), ..., (1,7), (2,0), ..., (2,7)  [size 2]
+   *   (0,8), ..., (0,15), (1,8), ..., (1,15), ...              [size 3]
+   */
+  Node d_virtual_enum;
   /**
    * The minimal n such that G_uq_n is not asserted negatively in the
    * current SAT context.
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 412d1b211..3d8052ae4 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -99,6 +99,7 @@ Node CegGrammarConstructor::process(Node q,
     Trace("cegqi") << "CegConjecture : collect constants..." << std::endl;
     collectTerms( q[1], extra_cons );
   }
+  std::map<TypeNode, std::vector<Node>> exc_cons;
 
   NodeManager* nm = NodeManager::currentNM();
 
@@ -140,20 +141,17 @@ Node CegGrammarConstructor::process(Node q,
       // check which arguments are irrelevant
       std::unordered_set<unsigned> arg_irrelevant;
       d_parent->getProcess()->getIrrelevantArgs(sf, arg_irrelevant);
-      std::unordered_set<Node, NodeHashFunction> term_irrelevant;
+      std::unordered_set<Node, NodeHashFunction> term_irlv;
       // convert to term
-      for (std::unordered_set<unsigned>::iterator ita = arg_irrelevant.begin();
-           ita != arg_irrelevant.end();
-           ++ita)
+      for (const unsigned& arg : arg_irrelevant)
       {
-        unsigned arg = *ita;
         Assert(arg < sfvl.getNumChildren());
-        term_irrelevant.insert(sfvl[arg]);
+        term_irlv.insert(sfvl[arg]);
       }
 
       // make the default grammar
       tn = mkSygusDefaultType(
-          preGrammarType, sfvl, ss.str(), extra_cons, term_irrelevant);
+          preGrammarType, sfvl, ss.str(), extra_cons, exc_cons, term_irlv);
     }
 
     // normalize type
@@ -389,7 +387,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
     TypeNode range,
     Node bvl,
     const std::string& fun,
-    std::map<TypeNode, std::vector<Node> >& extra_cons,
+    std::map<TypeNode, std::vector<Node>>& extra_cons,
+    std::map<TypeNode, std::vector<Node>>& exc_cons,
     std::unordered_set<Node, NodeHashFunction>& term_irrelevant,
     std::vector<CVC4::Datatype>& datatypes,
     std::set<Type>& unres)
@@ -589,8 +588,18 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
     }
     Trace("sygus-grammar-def") << "...make datatype " << datatypes[i] << std::endl;
     datatypes[i].setSygus( types[i].toType(), bvl.toExpr(), true, true );
-    for( unsigned j=0; j<ops[i].size(); j++ ){
-      datatypes[i].addSygusConstructor( ops[i][j], cnames[j], cargs[j] );
+    std::map<TypeNode, std::vector<Node>>::iterator itexc =
+        exc_cons.find(types[i]);
+    for (unsigned j = 0, size = ops[i].size(); j < size; j++)
+    {
+      // add the constructor if it is not excluded
+      Node opn = Node::fromExpr(ops[i][j]);
+      if (itexc == exc_cons.end()
+          || std::find(itexc->second.begin(), itexc->second.end(), opn)
+                 == itexc->second.end())
+      {
+        datatypes[i].addSygusConstructor(ops[i][j], cnames[j], cargs[j]);
+      }
     }
     Trace("sygus-grammar-def")
         << "...built datatype " << datatypes[i] << " ";
@@ -717,7 +726,8 @@ TypeNode CegGrammarConstructor::mkSygusDefaultType(
     TypeNode range,
     Node bvl,
     const std::string& fun,
-    std::map<TypeNode, std::vector<Node> >& extra_cons,
+    std::map<TypeNode, std::vector<Node>>& extra_cons,
+    std::map<TypeNode, std::vector<Node>>& exclude_cons,
     std::unordered_set<Node, NodeHashFunction>& term_irrelevant)
 {
   Trace("sygus-grammar-def") << "*** Make sygus default type " << range << ", make datatypes..." << std::endl;
@@ -726,8 +736,14 @@ TypeNode CegGrammarConstructor::mkSygusDefaultType(
   }
   std::set<Type> unres;
   std::vector< CVC4::Datatype > datatypes;
-  mkSygusDefaultGrammar(
-      range, bvl, fun, extra_cons, term_irrelevant, datatypes, unres);
+  mkSygusDefaultGrammar(range,
+                        bvl,
+                        fun,
+                        extra_cons,
+                        exclude_cons,
+                        term_irrelevant,
+                        datatypes,
+                        unres);
   Trace("sygus-grammar-def")  << "...made " << datatypes.size() << " datatypes, now make mutual datatype types..." << std::endl;
   Assert( !datatypes.empty() );
   std::vector<DatatypeType> types = NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(datatypes, unres);
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
index 39f95527f..578325fea 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
@@ -67,7 +67,8 @@ public:
  /** make the default sygus datatype type corresponding to builtin type range
  *   bvl is the set of free variables to include in the grammar
  *   fun is for naming
- *   extra_cons is a set of extra constant symbols to include in the grammar
+ *   extra_cons is a set of extra constant symbols to include in the grammar,
+ *   exclude_cons is used to exclude operators from the grammar,
  *   term_irrelevant is a set of terms that should not be included in the
  *      grammar.
  */
@@ -76,6 +77,7 @@ public:
      Node bvl,
      const std::string& fun,
      std::map<TypeNode, std::vector<Node> >& extra_cons,
+     std::map<TypeNode, std::vector<Node> >& exclude_cons,
      std::unordered_set<Node, NodeHashFunction>& term_irrelevant);
  /** make the default sygus datatype type corresponding to builtin type range */
  static TypeNode mkSygusDefaultType(TypeNode range,
@@ -83,8 +85,10 @@ public:
                                     const std::string& fun)
  {
    std::map<TypeNode, std::vector<Node> > extra_cons;
+   std::map<TypeNode, std::vector<Node> > exclude_cons;
    std::unordered_set<Node, NodeHashFunction> term_irrelevant;
-   return mkSygusDefaultType(range, bvl, fun, extra_cons, term_irrelevant);
+   return mkSygusDefaultType(
+       range, bvl, fun, extra_cons, exclude_cons, term_irrelevant);
   }
   /** make the sygus datatype type that encodes the solution space (lambda
   * templ_arg. templ[templ_arg]) where templ_arg
@@ -138,6 +142,7 @@ public:
       Node bvl,
       const std::string& fun,
       std::map<TypeNode, std::vector<Node> >& extra_cons,
+      std::map<TypeNode, std::vector<Node> >& exclude_cons,
       std::unordered_set<Node, NodeHashFunction>& term_irrelevant,
       std::vector<CVC4::Datatype>& datatypes,
       std::set<Type>& unres);
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 85ff5c896..5efa1198b 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -752,8 +752,14 @@ void TermDbSygus::registerEnumerator(Node e,
                                      CegConjecture* conj,
                                      bool mkActiveGuard)
 {
-  Assert(d_enum_to_conjecture.find(e) == d_enum_to_conjecture.end());
-  Trace("sygus-db") << "Register measured term : " << e << std::endl;
+  if (d_enum_to_conjecture.find(e) != d_enum_to_conjecture.end())
+  {
+    // already registered
+    return;
+  }
+  Trace("sygus-db") << "Register enumerator : " << e << std::endl;
+  // register its type
+  registerSygusType(e.getType());
   d_enum_to_conjecture[e] = conj;
   d_enum_to_synth_fun[e] = f;
   if( mkActiveGuard ){
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index a9e17fdf9..d53e436e0 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -38,7 +38,13 @@ class TermDbSygus {
   bool reset(Theory::Effort e);
   /** Identify this utility */
   std::string identify() const { return "TermDbSygus"; }
-  /** register the sygus type */
+  /** register the sygus type
+   *
+   * This initializes this database for sygus datatype type tn. This may
+   * throw an assertion failure if the sygus grammar has type errors. Otherwise,
+   * after registering a sygus type, the query functions in this class (such
+   * as sygusToBuiltinType, getKindConsNum, etc.) can be called for tn.
+   */
   void registerSygusType(TypeNode tn);
 
   //------------------------------utilities
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 687ed3c86..745183a6b 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1471,6 +1471,7 @@ REG1_TESTS = \
 	regress1/sygus/array_sum_2_5.sy \
 	regress1/sygus/cegar1.sy \
 	regress1/sygus/cegisunif-depth1.sy \
+	regress1/sygus/cegis-unif-inv-eq-fair.sy \
 	regress1/sygus/cggmp.sy \
 	regress1/sygus/clock-inc-tuple.sy \
 	regress1/sygus/commutative.sy \
diff --git a/test/regress/regress1/sygus/cegis-unif-inv-eq-fair.sy b/test/regress/regress1/sygus/cegis-unif-inv-eq-fair.sy
new file mode 100644
index 000000000..7d1c35234
--- /dev/null
+++ b/test/regress/regress1/sygus/cegis-unif-inv-eq-fair.sy
@@ -0,0 +1,536 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-unif --sygus-bool-ite-return-const --sygus-out=status
+(set-logic LIA)
+
+(define-fun
+  __node_init_Sofar_0 (
+    (Sofar.usr.X@0 Bool)
+    (Sofar.usr.Sofar@0 Bool)
+    (Sofar.res.init_flag@0 Bool)
+  ) Bool
+  
+  (and (= Sofar.usr.Sofar@0 Sofar.usr.X@0) Sofar.res.init_flag@0)
+)
+
+(define-fun
+  __node_trans_Sofar_0 (
+    (Sofar.usr.X@1 Bool)
+    (Sofar.usr.Sofar@1 Bool)
+    (Sofar.res.init_flag@1 Bool)
+    (Sofar.usr.X@0 Bool)
+    (Sofar.usr.Sofar@0 Bool)
+    (Sofar.res.init_flag@0 Bool)
+  ) Bool
+  
+  (and
+   (= Sofar.usr.Sofar@1 (and Sofar.usr.X@1 Sofar.usr.Sofar@0))
+   (not Sofar.res.init_flag@1))
+)
+
+(define-fun
+  __node_init_excludes2_0 (
+    (excludes2.usr.X1@0 Bool)
+    (excludes2.usr.X2@0 Bool)
+    (excludes2.usr.excludes@0 Bool)
+    (excludes2.res.init_flag@0 Bool)
+  ) Bool
+  
+  (and
+   (=
+    excludes2.usr.excludes@0
+    (not (and excludes2.usr.X1@0 excludes2.usr.X2@0)))
+   excludes2.res.init_flag@0)
+)
+
+(define-fun
+  __node_trans_excludes2_0 (
+    (excludes2.usr.X1@1 Bool)
+    (excludes2.usr.X2@1 Bool)
+    (excludes2.usr.excludes@1 Bool)
+    (excludes2.res.init_flag@1 Bool)
+    (excludes2.usr.X1@0 Bool)
+    (excludes2.usr.X2@0 Bool)
+    (excludes2.usr.excludes@0 Bool)
+    (excludes2.res.init_flag@0 Bool)
+  ) Bool
+  
+  (and
+   (=
+    excludes2.usr.excludes@1
+    (not (and excludes2.usr.X1@1 excludes2.usr.X2@1)))
+   (not excludes2.res.init_flag@1))
+)
+
+(define-fun
+  __node_init_voiture_0 (
+    (voiture.usr.m@0 Bool)
+    (voiture.usr.s@0 Bool)
+    (voiture.usr.toofast@0 Bool)
+    (voiture.usr.stop@0 Bool)
+    (voiture.usr.bump@0 Bool)
+    (voiture.usr.dist@0 Int)
+    (voiture.usr.speed@0 Int)
+    (voiture.usr.time@0 Int)
+    (voiture.usr.move@0 Bool)
+    (voiture.usr.second@0 Bool)
+    (voiture.usr.meter@0 Bool)
+    (voiture.res.init_flag@0 Bool)
+    (voiture.res.abs_0@0 Bool)
+  ) Bool
+  
+  (and
+   (= voiture.usr.speed@0 0)
+   (= voiture.usr.toofast@0 (>= voiture.usr.speed@0 3))
+   (= voiture.usr.move@0 true)
+   (= voiture.usr.time@0 0)
+   (= voiture.usr.dist@0 0)
+   (= voiture.usr.bump@0 (= voiture.usr.dist@0 10))
+   (= voiture.usr.stop@0 (>= voiture.usr.time@0 4))
+   (=
+    voiture.res.abs_0@0
+    (and
+     (and
+      (and voiture.usr.move@0 (not voiture.usr.stop@0))
+      (not voiture.usr.toofast@0))
+     (not voiture.usr.bump@0)))
+   (= voiture.usr.second@0 false)
+   (= voiture.usr.meter@0 false)
+   voiture.res.init_flag@0)
+)
+
+(define-fun
+  __node_trans_voiture_0 (
+    (voiture.usr.m@1 Bool)
+    (voiture.usr.s@1 Bool)
+    (voiture.usr.toofast@1 Bool)
+    (voiture.usr.stop@1 Bool)
+    (voiture.usr.bump@1 Bool)
+    (voiture.usr.dist@1 Int)
+    (voiture.usr.speed@1 Int)
+    (voiture.usr.time@1 Int)
+    (voiture.usr.move@1 Bool)
+    (voiture.usr.second@1 Bool)
+    (voiture.usr.meter@1 Bool)
+    (voiture.res.init_flag@1 Bool)
+    (voiture.res.abs_0@1 Bool)
+    (voiture.usr.m@0 Bool)
+    (voiture.usr.s@0 Bool)
+    (voiture.usr.toofast@0 Bool)
+    (voiture.usr.stop@0 Bool)
+    (voiture.usr.bump@0 Bool)
+    (voiture.usr.dist@0 Int)
+    (voiture.usr.speed@0 Int)
+    (voiture.usr.time@0 Int)
+    (voiture.usr.move@0 Bool)
+    (voiture.usr.second@0 Bool)
+    (voiture.usr.meter@0 Bool)
+    (voiture.res.init_flag@0 Bool)
+    (voiture.res.abs_0@0 Bool)
+  ) Bool
+  
+  (and
+   (= voiture.usr.meter@1 (and voiture.usr.m@1 (not voiture.usr.s@1)))
+   (= voiture.usr.second@1 voiture.usr.s@1)
+   (= voiture.usr.move@1 voiture.res.abs_0@0)
+   (=
+    voiture.usr.speed@1
+    (ite
+     (or (not voiture.usr.move@1) voiture.usr.second@1)
+     0
+     (ite
+      (and voiture.usr.move@1 voiture.usr.meter@1)
+      (+ (- voiture.usr.speed@0 1) 1)
+      voiture.usr.speed@0)))
+   (= voiture.usr.toofast@1 (>= voiture.usr.speed@1 3))
+   (=
+    voiture.usr.time@1
+    (ite voiture.usr.second@1 (+ voiture.usr.time@0 1) voiture.usr.time@0))
+   (=
+    voiture.usr.dist@1
+    (ite
+     (and voiture.usr.move@1 voiture.usr.meter@1)
+     (+ voiture.usr.dist@0 1)
+     voiture.usr.dist@0))
+   (= voiture.usr.bump@1 (= voiture.usr.dist@1 10))
+   (= voiture.usr.stop@1 (>= voiture.usr.time@1 4))
+   (=
+    voiture.res.abs_0@1
+    (and
+     (and
+      (and voiture.usr.move@1 (not voiture.usr.stop@1))
+      (not voiture.usr.toofast@1))
+     (not voiture.usr.bump@1)))
+   (not voiture.res.init_flag@1))
+)
+
+(define-fun
+  __node_init_top_0 (
+    (top.usr.m@0 Bool)
+    (top.usr.s@0 Bool)
+    (top.usr.OK@0 Bool)
+    (top.res.init_flag@0 Bool)
+    (top.res.abs_0@0 Bool)
+    (top.res.abs_1@0 Bool)
+    (top.res.abs_2@0 Bool)
+    (top.res.abs_3@0 Int)
+    (top.res.abs_4@0 Int)
+    (top.res.abs_5@0 Int)
+    (top.res.abs_6@0 Bool)
+    (top.res.abs_7@0 Bool)
+    (top.res.abs_8@0 Bool)
+    (top.res.abs_9@0 Bool)
+    (top.res.abs_10@0 Bool)
+    (top.res.inst_3@0 Bool)
+    (top.res.inst_2@0 Bool)
+    (top.res.inst_1@0 Bool)
+    (top.res.inst_0@0 Bool)
+  ) Bool
+  
+  (let
+   ((X1 Bool top.res.abs_10@0))
+   (let
+    ((X2 Int top.res.abs_4@0))
+    (and
+     (= top.usr.OK@0 (=> X1 (< X2 4)))
+     (__node_init_voiture_0
+      top.usr.m@0
+      top.usr.s@0
+      top.res.abs_0@0
+      top.res.abs_1@0
+      top.res.abs_2@0
+      top.res.abs_3@0
+      top.res.abs_4@0
+      top.res.abs_5@0
+      top.res.abs_6@0
+      top.res.abs_7@0
+      top.res.abs_8@0
+      top.res.inst_3@0
+      top.res.inst_2@0)
+     (__node_init_Sofar_0 top.res.abs_9@0 top.res.abs_10@0 top.res.inst_1@0)
+     (__node_init_excludes2_0
+      top.usr.m@0
+      top.usr.s@0
+      top.res.abs_9@0
+      top.res.inst_0@0)
+     top.res.init_flag@0)))
+)
+
+(define-fun
+  __node_trans_top_0 (
+    (top.usr.m@1 Bool)
+    (top.usr.s@1 Bool)
+    (top.usr.OK@1 Bool)
+    (top.res.init_flag@1 Bool)
+    (top.res.abs_0@1 Bool)
+    (top.res.abs_1@1 Bool)
+    (top.res.abs_2@1 Bool)
+    (top.res.abs_3@1 Int)
+    (top.res.abs_4@1 Int)
+    (top.res.abs_5@1 Int)
+    (top.res.abs_6@1 Bool)
+    (top.res.abs_7@1 Bool)
+    (top.res.abs_8@1 Bool)
+    (top.res.abs_9@1 Bool)
+    (top.res.abs_10@1 Bool)
+    (top.res.inst_3@1 Bool)
+    (top.res.inst_2@1 Bool)
+    (top.res.inst_1@1 Bool)
+    (top.res.inst_0@1 Bool)
+    (top.usr.m@0 Bool)
+    (top.usr.s@0 Bool)
+    (top.usr.OK@0 Bool)
+    (top.res.init_flag@0 Bool)
+    (top.res.abs_0@0 Bool)
+    (top.res.abs_1@0 Bool)
+    (top.res.abs_2@0 Bool)
+    (top.res.abs_3@0 Int)
+    (top.res.abs_4@0 Int)
+    (top.res.abs_5@0 Int)
+    (top.res.abs_6@0 Bool)
+    (top.res.abs_7@0 Bool)
+    (top.res.abs_8@0 Bool)
+    (top.res.abs_9@0 Bool)
+    (top.res.abs_10@0 Bool)
+    (top.res.inst_3@0 Bool)
+    (top.res.inst_2@0 Bool)
+    (top.res.inst_1@0 Bool)
+    (top.res.inst_0@0 Bool)
+  ) Bool
+  
+  (let
+   ((X1 Bool top.res.abs_10@1))
+   (let
+    ((X2 Int top.res.abs_4@1))
+    (and
+     (= top.usr.OK@1 (=> X1 (< X2 4)))
+     (__node_trans_voiture_0
+      top.usr.m@1
+      top.usr.s@1
+      top.res.abs_0@1
+      top.res.abs_1@1
+      top.res.abs_2@1
+      top.res.abs_3@1
+      top.res.abs_4@1
+      top.res.abs_5@1
+      top.res.abs_6@1
+      top.res.abs_7@1
+      top.res.abs_8@1
+      top.res.inst_3@1
+      top.res.inst_2@1
+      top.usr.m@0
+      top.usr.s@0
+      top.res.abs_0@0
+      top.res.abs_1@0
+      top.res.abs_2@0
+      top.res.abs_3@0
+      top.res.abs_4@0
+      top.res.abs_5@0
+      top.res.abs_6@0
+      top.res.abs_7@0
+      top.res.abs_8@0
+      top.res.inst_3@0
+      top.res.inst_2@0)
+     (__node_trans_Sofar_0
+      top.res.abs_9@1
+      top.res.abs_10@1
+      top.res.inst_1@1
+      top.res.abs_9@0
+      top.res.abs_10@0
+      top.res.inst_1@0)
+     (__node_trans_excludes2_0
+      top.usr.m@1
+      top.usr.s@1
+      top.res.abs_9@1
+      top.res.inst_0@1
+      top.usr.m@0
+      top.usr.s@0
+      top.res.abs_9@0
+      top.res.inst_0@0)
+     (not top.res.init_flag@1))))
+)
+
+
+
+(synth-inv str_invariant(
+  (top.usr.m Bool)
+  (top.usr.s Bool)
+  (top.usr.OK Bool)
+  (top.res.init_flag Bool)
+  (top.res.abs_0 Bool)
+  (top.res.abs_1 Bool)
+  (top.res.abs_2 Bool)
+  (top.res.abs_3 Int)
+  (top.res.abs_4 Int)
+  (top.res.abs_5 Int)
+  (top.res.abs_6 Bool)
+  (top.res.abs_7 Bool)
+  (top.res.abs_8 Bool)
+  (top.res.abs_9 Bool)
+  (top.res.abs_10 Bool)
+  (top.res.inst_3 Bool)
+  (top.res.inst_2 Bool)
+  (top.res.inst_1 Bool)
+  (top.res.inst_0 Bool)
+))
+
+
+(declare-primed-var top.usr.m Bool)
+(declare-primed-var top.usr.s Bool)
+(declare-primed-var top.usr.OK Bool)
+(declare-primed-var top.res.init_flag Bool)
+(declare-primed-var top.res.abs_0 Bool)
+(declare-primed-var top.res.abs_1 Bool)
+(declare-primed-var top.res.abs_2 Bool)
+(declare-primed-var top.res.abs_3 Int)
+(declare-primed-var top.res.abs_4 Int)
+(declare-primed-var top.res.abs_5 Int)
+(declare-primed-var top.res.abs_6 Bool)
+(declare-primed-var top.res.abs_7 Bool)
+(declare-primed-var top.res.abs_8 Bool)
+(declare-primed-var top.res.abs_9 Bool)
+(declare-primed-var top.res.abs_10 Bool)
+(declare-primed-var top.res.inst_3 Bool)
+(declare-primed-var top.res.inst_2 Bool)
+(declare-primed-var top.res.inst_1 Bool)
+(declare-primed-var top.res.inst_0 Bool)
+
+(define-fun
+  init (
+    (top.usr.m Bool)
+    (top.usr.s Bool)
+    (top.usr.OK Bool)
+    (top.res.init_flag Bool)
+    (top.res.abs_0 Bool)
+    (top.res.abs_1 Bool)
+    (top.res.abs_2 Bool)
+    (top.res.abs_3 Int)
+    (top.res.abs_4 Int)
+    (top.res.abs_5 Int)
+    (top.res.abs_6 Bool)
+    (top.res.abs_7 Bool)
+    (top.res.abs_8 Bool)
+    (top.res.abs_9 Bool)
+    (top.res.abs_10 Bool)
+    (top.res.inst_3 Bool)
+    (top.res.inst_2 Bool)
+    (top.res.inst_1 Bool)
+    (top.res.inst_0 Bool)
+  ) Bool
+  
+  (let
+   ((X1 Bool top.res.abs_10))
+   (let
+    ((X2 Int top.res.abs_4))
+    (and
+     (= top.usr.OK (=> X1 (< X2 4)))
+     (__node_init_voiture_0
+      top.usr.m
+      top.usr.s
+      top.res.abs_0
+      top.res.abs_1
+      top.res.abs_2
+      top.res.abs_3
+      top.res.abs_4
+      top.res.abs_5
+      top.res.abs_6
+      top.res.abs_7
+      top.res.abs_8
+      top.res.inst_3
+      top.res.inst_2)
+     (__node_init_Sofar_0 top.res.abs_9 top.res.abs_10 top.res.inst_1)
+     (__node_init_excludes2_0
+      top.usr.m
+      top.usr.s
+      top.res.abs_9
+      top.res.inst_0)
+     top.res.init_flag)))
+)
+
+(define-fun
+  trans (
+    
+    ;; Current state.
+    (top.usr.m Bool)
+    (top.usr.s Bool)
+    (top.usr.OK Bool)
+    (top.res.init_flag Bool)
+    (top.res.abs_0 Bool)
+    (top.res.abs_1 Bool)
+    (top.res.abs_2 Bool)
+    (top.res.abs_3 Int)
+    (top.res.abs_4 Int)
+    (top.res.abs_5 Int)
+    (top.res.abs_6 Bool)
+    (top.res.abs_7 Bool)
+    (top.res.abs_8 Bool)
+    (top.res.abs_9 Bool)
+    (top.res.abs_10 Bool)
+    (top.res.inst_3 Bool)
+    (top.res.inst_2 Bool)
+    (top.res.inst_1 Bool)
+    (top.res.inst_0 Bool)
+    
+    ;; Next state.
+    (top.usr.m! Bool)
+    (top.usr.s! Bool)
+    (top.usr.OK! Bool)
+    (top.res.init_flag! Bool)
+    (top.res.abs_0! Bool)
+    (top.res.abs_1! Bool)
+    (top.res.abs_2! Bool)
+    (top.res.abs_3! Int)
+    (top.res.abs_4! Int)
+    (top.res.abs_5! Int)
+    (top.res.abs_6! Bool)
+    (top.res.abs_7! Bool)
+    (top.res.abs_8! Bool)
+    (top.res.abs_9! Bool)
+    (top.res.abs_10! Bool)
+    (top.res.inst_3! Bool)
+    (top.res.inst_2! Bool)
+    (top.res.inst_1! Bool)
+    (top.res.inst_0! Bool)
+  
+  ) Bool
+  
+  (let
+   ((X1 Bool top.res.abs_10!))
+   (let
+    ((X2 Int top.res.abs_4!))
+    (and
+     (= top.usr.OK! (=> X1 (< X2 4)))
+     (__node_trans_voiture_0
+      top.usr.m!
+      top.usr.s!
+      top.res.abs_0!
+      top.res.abs_1!
+      top.res.abs_2!
+      top.res.abs_3!
+      top.res.abs_4!
+      top.res.abs_5!
+      top.res.abs_6!
+      top.res.abs_7!
+      top.res.abs_8!
+      top.res.inst_3!
+      top.res.inst_2!
+      top.usr.m
+      top.usr.s
+      top.res.abs_0
+      top.res.abs_1
+      top.res.abs_2
+      top.res.abs_3
+      top.res.abs_4
+      top.res.abs_5
+      top.res.abs_6
+      top.res.abs_7
+      top.res.abs_8
+      top.res.inst_3
+      top.res.inst_2)
+     (__node_trans_Sofar_0
+      top.res.abs_9!
+      top.res.abs_10!
+      top.res.inst_1!
+      top.res.abs_9
+      top.res.abs_10
+      top.res.inst_1)
+     (__node_trans_excludes2_0
+      top.usr.m!
+      top.usr.s!
+      top.res.abs_9!
+      top.res.inst_0!
+      top.usr.m
+      top.usr.s
+      top.res.abs_9
+      top.res.inst_0)
+     (not top.res.init_flag!))))
+)
+
+(define-fun
+  prop (
+    (top.usr.m Bool)
+    (top.usr.s Bool)
+    (top.usr.OK Bool)
+    (top.res.init_flag Bool)
+    (top.res.abs_0 Bool)
+    (top.res.abs_1 Bool)
+    (top.res.abs_2 Bool)
+    (top.res.abs_3 Int)
+    (top.res.abs_4 Int)
+    (top.res.abs_5 Int)
+    (top.res.abs_6 Bool)
+    (top.res.abs_7 Bool)
+    (top.res.abs_8 Bool)
+    (top.res.abs_9 Bool)
+    (top.res.abs_10 Bool)
+    (top.res.inst_3 Bool)
+    (top.res.inst_2 Bool)
+    (top.res.inst_1 Bool)
+    (top.res.inst_0 Bool)
+  ) Bool
+  
+  top.usr.OK
+)
+
+(inv-constraint str_invariant init trans prop)
+
+(check-synth)