Mark datatypes as sygus. Add option to normalize sygus terms in search. Add sygus regressions.

15 files changed, 300 insertions, 17 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index d2f38cc82..a83299d3b 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -600,6 +600,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
         std::string dname = ss.str();
         sorts.push_back(t);
         datatypes.push_back(Datatype(dname));
+        datatypes.back().setSygusType( t );
         ops.push_back(std::vector<Expr>());
         cnames.push_back(std::vector<std::string>());
         cargs.push_back(std::vector<std::vector<CVC4::Type> >());
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 077f385b0..c6c3a896c 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -534,7 +534,7 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
     testerId.append(name);
     checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
     checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE);
-    CVC4::DatatypeConstructor c(name, testerId);
+    CVC4::DatatypeConstructor c(name, testerId, ops[i] );
     for( unsigned j=0; j<cargs[i].size(); j++ ){
       std::stringstream sname;
       sname << name << "_" << j;
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index bf986a138..8db9435ed 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -238,11 +238,16 @@ void TheoryDatatypes::check(Effort e) {
                 }else{
                   Trace("dt-split") << "*************Split for constructors on " << n <<  endl;
                   std::vector< Node > children;
-                  for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-                    Node test = DatatypesRewriter::mkTester( n, i, dt );
-                    children.push_back( test );
+                  if( dt.isSygus() && options::sygusNormalForm() ){
+                    getSygusSplits( n, dt, children );
+                  }else{
+                    for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+                      Node test = DatatypesRewriter::mkTester( n, i, dt );
+                      children.push_back( test );
+                    }
                   }
-                  Node lemma = NodeManager::currentNM()->mkNode( kind::OR, children );
+                  Assert( !children.empty() );
+                  Node lemma = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( kind::OR, children );
                   d_out->lemma( lemma );
                 }
                 return;
@@ -294,10 +299,10 @@ void TheoryDatatypes::flushPendingFacts(){
       Node exp = d_pending_exp[ fact ];
       //check to see if we have to communicate it to the rest of the system
       if( mustCommunicateFact( fact, exp ) ){
-        Trace("dt-lemma-debug") << "Assert fact " << fact << " " << exp << std::endl;
+        Trace("dt-lemma-debug") << "Assert fact " << fact << " with explanation " << exp << std::endl;
         Node lem = fact;
         if( exp.isNull() || exp==d_true ){
-          lem = fact;
+          Trace("dt-lemma-debug") << "Trivial explanation." << std::endl;
         }else{
           Trace("dt-lemma-debug") << "Get explanation..." << std::endl;
           Node ee_exp = explain( exp );
@@ -394,12 +399,7 @@ Node TheoryDatatypes::expandDefinition(LogicRequest &logicRequest, Node n) {
       if( tst==d_true ){
         n_ret = sel;
       }else{
-        if( d_exp_def_skolem.find( selector )==d_exp_def_skolem.end() ){
-          std::stringstream ss;
-          ss << selector << "_uf";
-          d_exp_def_skolem[ selector ] = NodeManager::currentNM()->mkSkolem( ss.str().c_str(),
-                                            NodeManager::currentNM()->mkFunctionType( n[0].getType(), n.getType() ) );
-        }
+        mkExpDefSkolem( selector, n[0].getType(), n.getType() );
         Node sk = NodeManager::currentNM()->mkNode( kind::APPLY_UF, d_exp_def_skolem[ selector ], n[0]  );
         if( tst==NodeManager::currentNM()->mkConst( false ) ){
           n_ret = sk;
@@ -694,7 +694,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
         if( !cons1.isNull() && !cons2.isNull() ){
           Debug("datatypes-debug") << "Constructors : " << cons1 << " " << cons2 << std::endl;
           Node unifEq = cons1.eqNode( cons2 );
-#if 0
+          /*
           std::vector< Node > exp;
           std::vector< std::pair< TNode, TNode > > deq_cand;
           bool conf = checkClashModEq( cons1, cons2, exp, deq_cand );
@@ -711,11 +711,10 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
           if( conf ){
             exp.push_back( unifEq );
             d_conflictNode = explain( exp );
-#else
+         */
           std::vector< Node > rew;
           if( DatatypesRewriter::checkClash( cons1, cons2, rew ) ){
             d_conflictNode = explain( unifEq );
-#endif
             Trace("dt-conflict") << "CONFLICT: Clash conflict : " << d_conflictNode << std::endl;
             d_out->conflict( d_conflictNode );
             d_conflict = true;
@@ -864,6 +863,15 @@ void TheoryDatatypes::getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool >
   }
 }
 
+void TheoryDatatypes::mkExpDefSkolem( Node sel, TypeNode dt, TypeNode rt ) {
+  if( d_exp_def_skolem.find( sel )==d_exp_def_skolem.end() ){
+    std::stringstream ss;
+    ss << sel << "_uf";
+    d_exp_def_skolem[ sel ] = NodeManager::currentNM()->mkSkolem( ss.str().c_str(),
+                                  NodeManager::currentNM()->mkFunctionType( dt, rt ) );
+  }
+}
+
 void TheoryDatatypes::addTester( Node t, EqcInfo* eqc, Node n ){
   Debug("datatypes-debug") << "Add tester : " << t << " to eqc(" << n << ")" << std::endl;
   Debug("datatypes-labels") << "Add tester " << t << " " << n << " " << eqc << std::endl;
@@ -1032,8 +1040,15 @@ void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){
 }
 
 void TheoryDatatypes::collapseSelector( Node s, Node c ) {
+  Assert( c.getKind()==APPLY_CONSTRUCTOR );
+  Trace("dt-collapse-sel") << "collapse selector : " << s << " " << c << std::endl;
   Node r;
   if( s.getKind()==kind::APPLY_SELECTOR_TOTAL ){
+    //Trace("dt-collapse-sel") << "Indices : " << Datatype::indexOf(c.getOperator().toExpr()) << " " << Datatype::cindexOf(s.getOperator().toExpr()) << std::endl;
+    //if( Datatype::indexOf(c.getOperator().toExpr())!=Datatype::cindexOf(s.getOperator().toExpr()) ){
+    //  mkExpDefSkolem( s.getOperator(), s[0].getType(), s.getType() );
+    //  r = NodeManager::currentNM()->mkNode( kind::APPLY_UF, d_exp_def_skolem[s.getOperator().toExpr()], s[0] );
+    //}else{
     r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, s.getOperator(), c );
   }else if( s.getKind()==kind::DT_SIZE ){
     r = NodeManager::currentNM()->mkNode( kind::DT_SIZE, c );
@@ -1901,3 +1916,39 @@ bool TheoryDatatypes::checkClashModEq( TNode n1, TNode n2, std::vector< Node >&
   return false;
 }
 
+void TheoryDatatypes::getSygusSplits( Node n, const Datatype& dt, std::vector< Node >& splits ) {
+  Assert( dt.isSygus() );
+  Trace("sygus-split") << "Get sygus splits " << n << std::endl;
+  if( n.getKind()==APPLY_SELECTOR_TOTAL ){
+    Node op = n.getOperator();
+    std::map< Node, std::vector< bool > >::iterator it = d_sygus_splits.find( op );
+    if( it==d_sygus_splits.end() ){
+      Expr selectorExpr = op.toExpr();
+      int csIndex = Datatype::cindexOf(selectorExpr);
+      int sIndex = Datatype::indexOf(selectorExpr);
+      Trace("sygus-split") << "  Constructor, selector index : " << csIndex << " " << sIndex << std::endl;
+      for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+        Expr sop = dt[i].getSygusOp();
+        Kind sk = NodeManager::operatorToKind( Node::fromExpr( sop ) );
+        Trace("sygus-split") << "  Operator #" << i << " : " << sop << ", kind = " << sk << std::endl;
+        bool addSplit = true;
+        //TODO
+        
+        d_sygus_splits[op].push_back( addSplit );
+      }
+    }
+    for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+      if( d_sygus_splits[op][i] ){
+        Node test = DatatypesRewriter::mkTester( n, i, dt );
+        splits.push_back( test );
+      }
+    }
+    Assert( !splits.empty() );
+  }else{
+    for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+      Node test = DatatypesRewriter::mkTester( n, i, dt );
+      splits.push_back( test );
+    }
+  }
+}
+
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 30b0140a9..2f0ec20ec 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -133,6 +133,8 @@ private:
   bool hasTester( Node n );
   /** get the possible constructors for n */
   void getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool >& cons );
+  /** mkExpDefSkolem */
+  void mkExpDefSkolem( Node sel, TypeNode dt, TypeNode rt );
 private:
   /** The notify class */
   NotifyClass d_notify;
@@ -178,6 +180,8 @@ private:
   unsigned d_dtfCounter;
   /** expand definition skolem functions */
   std::map< Node, Node > d_exp_def_skolem;
+  /** sygus splits */
+  std::map< Node, std::vector< bool > > d_sygus_splits;
 private:
   /** assert fact */
   void assertFact( Node fact, Node exp );
@@ -276,6 +280,8 @@ private:
   bool mustCommunicateFact( Node n, Node exp );
   /** check clash mod eq */
   bool checkClashModEq( TNode n1, TNode n2, std::vector< Node >& exp, std::vector< std::pair< TNode, TNode > >& deq_cand );
+  /** get sygus splits */
+  void getSygusSplits( Node n, const Datatype& dt, std::vector< Node >& splits );
 private:
   //equality queries
   bool hasTerm( TNode a );
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index fc59b22b7..ad1508716 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -200,6 +200,8 @@ option sygusMinGrammar --sygus-min-grammar bool :default false
   minimize sygus grammars
 option sygusDecompose --sygus-decompose bool :default false
   decompose single invocation synthesis conjectures
+option sygusNormalForm --sygus-normal-form bool :default true
+  only search for sygus builtin terms that are in normal form
  
 
 option localTheoryExt --local-t-ext bool :default false
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index 7813626a7..c15e103f9 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -140,6 +140,14 @@ void Datatype::addConstructor(const DatatypeConstructor& c) {
   d_constructors.push_back(c);
 }
 
+
+void Datatype::setSygusType( Type st ){
+  CheckArgument(!d_resolved, this,
+                "cannot set sygus type to a finalized Datatype");
+  d_sygus_type = st;
+}
+
+
 Cardinality Datatype::getCardinality() const throw(IllegalArgumentException) {
   CheckArgument(isResolved(), this, "this datatype is not yet resolved");
 
@@ -543,6 +551,15 @@ DatatypeConstructor::DatatypeConstructor(std::string name, std::string tester) :
   CheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester");
 }
 
+DatatypeConstructor::DatatypeConstructor(std::string name, std::string tester, Expr sygus_op) :
+  d_name(name + '\0' + tester),
+  d_tester(),
+  d_args(),
+  d_sygus_op(sygus_op) {
+  CheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
+  CheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester");
+}
+
 void DatatypeConstructor::addArg(std::string selectorName, Type selectorType) {
   // We don't want to introduce a new data member, because eventually
   // we're going to be a constant stuffed inside a node.  So we stow
@@ -611,6 +628,11 @@ Expr DatatypeConstructor::getTester() const {
   return d_tester;
 }
 
+Expr DatatypeConstructor::getSygusOp() const {
+  CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+  return d_sygus_op;
+}
+
 Cardinality DatatypeConstructor::getCardinality() const throw(IllegalArgumentException) {
   CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 
diff --git a/src/util/datatype.h b/src/util/datatype.h
index 32fae8235..084202956 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -185,6 +185,8 @@ private:
   Expr d_constructor;
   Expr d_tester;
   std::vector<DatatypeConstructorArg> d_args;
+  /** the operator associated with this constructor (for sygus) */
+  Expr d_sygus_op;
 
   void resolve(ExprManager* em, DatatypeType self,
                const std::map<std::string, DatatypeType>& resolutions,
@@ -223,6 +225,7 @@ public:
    * constructor and tester aren't created until resolution time.
    */
   DatatypeConstructor(std::string name, std::string tester);
+  DatatypeConstructor(std::string name, std::string tester, Expr sygus_op);
 
   /**
    * Add an argument (i.e., a data field) of the given name and type
@@ -268,6 +271,9 @@ public:
    * Datatype must be resolved.
    */
   Expr getTester() const;
+  
+  /** get sygus op */
+  Expr getSygusOp() const;
 
   /**
    * Get the tester name for this Datatype constructor.
@@ -453,6 +459,7 @@ private:
   bool d_resolved;
   Type d_self;
   bool d_involvesExt;
+  Type d_sygus_type;
 
   // "mutable" because computing the cardinality can be expensive,
   // and so it's computed just once, on demand---this is the cache
@@ -510,6 +517,9 @@ public:
    */
   void addConstructor(const DatatypeConstructor& c);
 
+  /** set the sygus type of this datatype */
+  void setSygusType( Type st );
+  
   /** Get the name of this Datatype. */
   inline std::string getName() const throw();
 
@@ -530,6 +540,9 @@ public:
 
   /** is this a co-datatype? */
   inline bool isCodatatype() const;
+  
+  /** is this a sygus datatype? */
+  inline bool isSygus() const;
 
   /**
    * Return the cardinality of this datatype (the sum of the
@@ -720,6 +733,10 @@ inline bool Datatype::isCodatatype() const {
   return d_isCo;
 }
 
+inline bool Datatype::isSygus() const {
+  return !d_sygus_type.isNull();
+}
+
 inline bool Datatype::operator!=(const Datatype& other) const throw() {
   return !(*this == other);
 }
diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am
index ad1296af0..b5ea8b476 100644
--- a/test/regress/regress0/sygus/Makefile.am
+++ b/test/regress/regress0/sygus/Makefile.am
@@ -18,7 +18,12 @@ MAKEFLAGS = -k
 # These are run for all build profiles.
 # If a test shouldn't be run in e.g. competition mode,
 # put it below in "TESTS +="
-TESTS =
+TESTS = hd-01-d1-prog.sy \
+        icfp_28_10.sy \
+        commutative.sy \
+        constant.sy \
+        multi-fun-polynomial2.sy \
+        unbdd_inv_gen_winf1.sy
 
 # sygus tests currently taking too long for make regress
 EXTRA_DIST = $(TESTS) \
diff --git a/test/regress/regress0/sygus/commutative.sy b/test/regress/regress0/sygus/commutative.sy
new file mode 100644
index 000000000..15567b0a8
--- /dev/null
+++ b/test/regress/regress0/sygus/commutative.sy
@@ -0,0 +1,22 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi
+
+(set-logic LIA)
+
+(synth-fun comm ((x Int) (y Int)) Int
+    ((Start Int (x
+                 y
+                 (+ Start Start)
+                 (- Start Start)
+                 ))
+          ))
+
+(declare-var x Int)
+(declare-var y Int)
+
+(constraint (= (comm x y) (comm y x)))
+
+
+(check-synth)
+
+; (+ x y) is a valid solution
\ No newline at end of file
diff --git a/test/regress/regress0/sygus/constant.sy b/test/regress/regress0/sygus/constant.sy
new file mode 100644
index 000000000..ddc12a6a9
--- /dev/null
+++ b/test/regress/regress0/sygus/constant.sy
@@ -0,0 +1,23 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi
+
+(set-logic LIA)
+
+(synth-fun constant ((x Int)) Int
+    ((Start Int (x
+                 0
+                 1
+                 (+ Start Start)
+                 (- Start Start)
+                 ))
+          ))
+
+(declare-var x Int)
+(declare-var y Int)
+
+(constraint (= (constant x) (constant y)))
+
+
+(check-synth)
+
+; 0, 1, (- x x) are valid solutions
\ No newline at end of file
diff --git a/test/regress/regress0/sygus/hd-01-d1-prog.sy b/test/regress/regress0/sygus/hd-01-d1-prog.sy
new file mode 100644
index 000000000..a58bc2f64
--- /dev/null
+++ b/test/regress/regress0/sygus/hd-01-d1-prog.sy
@@ -0,0 +1,22 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi
+
+(set-logic BV)
+
+(define-fun hd01 ((x (BitVec 32))) (BitVec 32) (bvand x (bvsub x #x00000001)))
+
+(synth-fun f ((x (BitVec 32))) (BitVec 32)
+    ((Start (BitVec 32) ((bvand Start Start)
+                         (bvsub Start Start)
+						 (bvor Start Start)
+						 (bvadd Start Start)
+						 (bvxor Start Start)
+                         x
+						 #x00000000
+						 #xFFFFFFFF
+                         #x00000001))))
+
+(declare-var x (BitVec 32))
+(constraint (= (hd01 x) (f x)))
+(check-synth)
+
diff --git a/test/regress/regress0/sygus/icfp_28_10.sy b/test/regress/regress0/sygus/icfp_28_10.sy
new file mode 100644
index 000000000..6e1610337
--- /dev/null
+++ b/test/regress/regress0/sygus/icfp_28_10.sy
@@ -0,0 +1,40 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi
+
+(set-logic BV)
+
+(define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001))
+(define-fun shr4 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000004))
+(define-fun shr16 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000010))
+(define-fun shl1 ((x (BitVec 64))) (BitVec 64) (bvshl x #x0000000000000001))
+(define-fun if0 ((x (BitVec 64)) (y (BitVec 64)) (z (BitVec 64))) (BitVec 64) (ite (= x #x0000000000000001) y z))
+
+(synth-fun f ( (x (BitVec 64))) (BitVec 64)
+(
+
+(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)
+                    (shl1 Start)
+ 		    (shr1 Start)
+		    (shr4 Start)
+		    (shr16 Start)
+		    (bvand Start Start)
+		    (bvor Start Start)
+		    (bvxor Start Start)
+		    (bvadd Start Start)
+		    (if0 Start Start Start)
+ ))
+)
+)
+
+
+(constraint (= (f #xd74594057974e439) #x0000d74594057974))
+(constraint (= (f #x74641ebeee92e8a2) #x000074641ebeee92))
+(constraint (= (f #x91c80141d7ec76b1) #x000091c80141d7ec))
+(constraint (= (f #xe4e55862e5ee4bec) #x0000e4e55862e5ee))
+(constraint (= (f #x367da67ede4260ce) #x0000367da67ede42))
+(constraint (= (f #xa365eb36246b3d8e) #x0000a365eb36246b))
+(constraint (= (f #xcd8a44a6d4c09c29) #x0000cd8a44a6d4c0))
+(constraint (= (f #xa97e9b9b7970433d) #x0000a97e9b9b7970))
+(constraint (= (f #x474dec0dd75d6894) #x0000474dec0dd75d))
+(constraint (= (f #x12430014ed058b24) #x000012430014ed05))
+(check-synth)
diff --git a/test/regress/regress0/sygus/max.sl b/test/regress/regress0/sygus/max.sl
index aea8e8186..fdd925196 100644
--- a/test/regress/regress0/sygus/max.sl
+++ b/test/regress/regress0/sygus/max.sl
@@ -1,4 +1,5 @@
 ; EXPECT: unsat
+; COMMAND-LINE: --cegqi
 (set-logic LIA)
 
 (synth-fun max ((x Int) (y Int)) Int
diff --git a/test/regress/regress0/sygus/multi-fun-polynomial2.sy b/test/regress/regress0/sygus/multi-fun-polynomial2.sy
new file mode 100644
index 000000000..24d49ee4e
--- /dev/null
+++ b/test/regress/regress0/sygus/multi-fun-polynomial2.sy
@@ -0,0 +1,35 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi
+
+(set-logic LIA)
+
+(synth-fun addExpr1 ((x Int) (y Int)) Int
+    ((Start Int (x
+                 y
+		 0
+		 1
+                 (+ Start Start)
+                 (- Start Start)
+                 ))
+          ))
+
+(synth-fun addExpr2 ((x Int) (y Int)) Int
+    ((Start Int (x
+                 y
+		 0
+		 1
+                 (+ Start Start)
+                 (- Start Start)
+                 ))
+          ))
+
+
+(declare-var x Int)
+(declare-var y Int)
+
+(constraint (= (+ (addExpr1 x y) (addExpr2 y x)) (- x y)))
+
+
+(check-synth)
+
+; (x, y), (x-y, 0) ... are valid solutions
\ No newline at end of file
diff --git a/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy b/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy
new file mode 100644
index 000000000..dc39efd84
--- /dev/null
+++ b/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy
@@ -0,0 +1,36 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi
+
+(set-logic LIA)
+(synth-fun inv ((x Int)) Bool
+    (
+        (Start Bool ((and AtomicFormula AtomicFormula)
+                     (or AtomicFormula AtomicFormula)))
+        (AtomicFormula Bool ((<= Sum Const) (= Sum Const)))
+        (Sum Int ((+ Term Term)))
+        (Term Int ((* Sign Var)))
+        (Sign Int (0 1 -1))
+        (Var Int (x))
+        (Const Int ((+ Const Const) (- Const Const) 0 1))
+    )
+)
+
+(define-fun implies ((b1 Bool) (b2 Bool)) Bool (or (not b1) b2))
+(define-fun and3 ((b1 Bool) (b2 Bool) (b3 Bool)) Bool (and (and b1 b2) b3))
+(define-fun and4 ((b1 Bool) (b2 Bool) (b3 Bool) (b4 Bool)) Bool (and (and3 b1 b2 b3) b4))
+(define-fun and5 ((b1 Bool) (b2 Bool) (b3 Bool) (b4 Bool) (b5 Bool)) Bool (and (and4 b1 b2 b3 b4) b5))
+(define-fun and6 ((b1 Bool) (b2 Bool) (b3 Bool) (b4 Bool) (b5 Bool) (b6 Bool)) Bool (and (and5 b1 b2 b3 b4 b5) b6))
+(define-fun or3 ((b1 Bool) (b2 Bool) (b3 Bool)) Bool (or (or b1 b2) b3))
+(define-fun or4 ((b1 Bool) (b2 Bool) (b3 Bool) (b4 Bool)) Bool (or (or3 b1 b2 b3) b4))
+(define-fun or5 ((b1 Bool) (b2 Bool) (b3 Bool) (b4 Bool) (b5 Bool)) Bool (or (or4 b1 b2 b3 b4) b5))
+
+(declare-var s Int)
+
+(declare-var x Int)
+
+(constraint (implies (= x 0) (inv x)))
+(constraint (implies (inv x) (= x 0)))
+(constraint (implies (inv x) (inv x)))
+(constraint (implies (and (inv x) false) (not (= x 0))))
+
+(check-synth)