From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 7 Aug 2018 22:34:00 +0000 (-0500)
Subject: Fix inference of pre and post conditions for non variable arguments. (#2237)
X-Git-Tag: cvc5-1.0.0~4807
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ba99b080d20d521603635a1f0b57be1436eca731;p=cvc5.git

Fix inference of pre and post conditions for non variable arguments. (#2237)
---

diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index 9a6fad52a..6a7eb8197 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -770,6 +770,7 @@ void TransitionInference::getConstantSubstitution( std::vector< Node >& vars, st
 }
 
 void TransitionInference::process( Node n ) {
+  NodeManager* nm = NodeManager::currentNM();
   d_complete = true;
   std::vector< Node > n_check;
   if( n.getKind()==AND ){
@@ -787,28 +788,29 @@ void TransitionInference::process( Node n ) {
     Trace("cegqi-inv") << "TransitionInference : Process disjunct : " << nn << std::endl;
     if( processDisjunct( nn, terms, disjuncts, visited, true ) ){
       if( !terms.empty() ){
-        Node norm_args;
+        Node curr;
         int comp_num;
         std::map< bool, Node >::iterator itt = terms.find( false );
         if( itt!=terms.end() ){
-          norm_args = itt->second;
+          curr = itt->second;
           if( terms.find( true )!=terms.end() ){
             comp_num = 0;
           }else{
             comp_num = -1;
           }
         }else{
-          norm_args = terms[true];
+          curr = terms[true];
           comp_num = 1;
         }
-        std::vector< Node > subs;
-        for( unsigned j=0; j<norm_args.getNumChildren(); j++ ){
-          subs.push_back( norm_args[j] );
-        }        
-        Trace("cegqi-inv-debug2") << "  normalize based on " << norm_args << std::endl;
-        Assert( d_vars.size()==subs.size() );
+        Trace("cegqi-inv-debug2")
+            << "  normalize based on " << curr << std::endl;
+        std::vector<Node> vars;
+        std::vector<Node> svars;
+        getNormalizedSubstitution(curr, d_vars, vars, svars, disjuncts);
         for( unsigned j=0; j<disjuncts.size(); j++ ){
-          disjuncts[j] = Rewriter::rewrite( disjuncts[j].substitute( subs.begin(), subs.end(), d_vars.begin(), d_vars.end() ) );
+          Trace("cegqi-inv-debug2") << "  apply " << disjuncts[j] << std::endl;
+          disjuncts[j] = Rewriter::rewrite(disjuncts[j].substitute(
+              vars.begin(), vars.end(), svars.begin(), svars.end()));
           Trace("cegqi-inv-debug2") << "  ..." << disjuncts[j] << std::endl;
         }
         std::vector< Node > const_var;
@@ -817,23 +819,32 @@ void TransitionInference::process( Node n ) {
           //transition
           Assert( terms.find( true )!=terms.end() );
           Node next = terms[true];
-          next = Rewriter::rewrite( next.substitute( subs.begin(), subs.end(), d_vars.begin(), d_vars.end() ) );
+          next = Rewriter::rewrite(next.substitute(
+              vars.begin(), vars.end(), svars.begin(), svars.end()));
           Trace("cegqi-inv-debug") << "transition next predicate : " << next << std::endl;
-          // normalize the other direction
-          std::vector< Node > rvars;
-          for( unsigned i=0; i<next.getNumChildren(); i++ ){
-            rvars.push_back( next[i] );
-          }
-          if( d_prime_vars.size()<next.getNumChildren() ){
-            for( unsigned i=0; i<next.getNumChildren(); i++ ){
-              Node v = NodeManager::currentNM()->mkSkolem( "ir", next[i].getType(), "template inference rev argument" );
+          // make the primed variables if we have not already
+          if (d_prime_vars.empty())
+          {
+            for (unsigned j = 0, nchild = next.getNumChildren(); j < nchild;
+                 j++)
+            {
+              Node v = nm->mkSkolem(
+                  "ir", next[j].getType(), "template inference rev argument");
               d_prime_vars.push_back( v );
             }
           }
+          // normalize the other direction
           Trace("cegqi-inv-debug2") << "  normalize based on " << next << std::endl;
-          Assert( d_vars.size()==subs.size() );
+          std::vector<Node> rvars;
+          std::vector<Node> rsvars;
+          getNormalizedSubstitution(
+              next, d_prime_vars, rvars, rsvars, disjuncts);
+          Assert(rvars.size() == rsvars.size());
           for( unsigned j=0; j<disjuncts.size(); j++ ){
-            disjuncts[j] = Rewriter::rewrite( disjuncts[j].substitute( rvars.begin(), rvars.end(), d_prime_vars.begin(), d_prime_vars.end() ) );
+            Trace("cegqi-inv-debug2")
+                << "  apply " << disjuncts[j] << std::endl;
+            disjuncts[j] = Rewriter::rewrite(disjuncts[j].substitute(
+                rvars.begin(), rvars.end(), rsvars.begin(), rsvars.end()));
             Trace("cegqi-inv-debug2") << "  ..." << disjuncts[j] << std::endl;
           }
           getConstantSubstitution( d_prime_vars, disjuncts, const_var, const_subs, false );
@@ -889,6 +900,31 @@ void TransitionInference::process( Node n ) {
     d_com[i].d_this = ret;
   }
 }
+void TransitionInference::getNormalizedSubstitution(
+    Node curr,
+    const std::vector<Node>& pvars,
+    std::vector<Node>& vars,
+    std::vector<Node>& subs,
+    std::vector<Node>& disjuncts)
+{
+  for (unsigned j = 0, nchild = curr.getNumChildren(); j < nchild; j++)
+  {
+    if (curr[j].getKind() == BOUND_VARIABLE)
+    {
+      // if the argument is a bound variable, add to the renaming
+      vars.push_back(curr[j]);
+      subs.push_back(pvars[j]);
+    }
+    else
+    {
+      // otherwise, treat as a constraint on the variable
+      // For example, this transforms e.g. a precondition clause
+      // I( 0, 1 ) to x1 != 0 OR x2 != 1 OR I( x1, x2 ).
+      Node eq = curr[j].eqNode(pvars[j]);
+      disjuncts.push_back(eq.negate());
+    }
+  }
+}
 
 bool TransitionInference::processDisjunct( Node n, std::map< bool, Node >& terms, std::vector< Node >& disjuncts, 
                                            std::map< Node, bool >& visited, bool topLevel ) {
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
index b368a0689..00b50a4a1 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
@@ -64,7 +64,29 @@ private:
   bool processDisjunct( Node n, std::map< bool, Node >& terms, std::vector< Node >& disjuncts, std::map< Node, bool >& visited, bool topLevel );
   void getConstantSubstitution( std::vector< Node >& vars, std::vector< Node >& disjuncts, std::vector< Node >& const_var, std::vector< Node >& const_subs, bool reqPol );
   bool d_complete;
-public:
+  /** get normalized substitution
+   *
+   * This method takes as input a node curr of the form I( t1, ..., tn ) and
+   * a vector of variables pvars, where pvars.size()=n. For each ti that is
+   * a variable, it adds ti to vars, and pvars[i] to subs. For each ti that is
+   * not a variable, it adds the disequality ti != pvars[i] to disjuncts.
+   *
+   * This function is used for instance to normalize an arbitrary application of
+   * I so that is over arguments pvars. For instance if curr is I(3,5,y) and
+   * pvars = { x1,x2,x3 }, then the formula:
+   *   I(3,5,y) ^ P(y)
+   * is equivalent to:
+   *   x1 != 3 V x2 != 5 V I(x1,x2,x3) V P( y ) { y -> x3 }
+   * Here, we add y and x3 to vars and subs respectively, and x1!=3 and x2!=5
+   * to disjuncts.
+   */
+  void getNormalizedSubstitution(Node curr,
+                                 const std::vector<Node>& pvars,
+                                 std::vector<Node>& vars,
+                                 std::vector<Node>& subs,
+                                 std::vector<Node>& disjuncts);
+
+ public:
   TransitionInference() : d_complete( false ) {}
   std::vector< Node > d_vars;
   std::vector< Node > d_prime_vars;
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index aec72993c..2be59087b 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -606,6 +606,7 @@ REG0_TESTS = \
 	regress0/quantifiers/ex3.smt2 \
 	regress0/quantifiers/ex6.smt2 \
 	regress0/quantifiers/floor.smt2 \
+	regress0/quantifiers/horn-ground-pre-post.smt2 \
 	regress0/quantifiers/is-even-pred.smt2 \
 	regress0/quantifiers/is-int.smt2 \
 	regress0/quantifiers/issue1805.smt2 \
diff --git a/test/regress/regress0/quantifiers/horn-ground-pre-post.smt2 b/test/regress/regress0/quantifiers/horn-ground-pre-post.smt2
new file mode 100644
index 000000000..082df249b
--- /dev/null
+++ b/test/regress/regress0/quantifiers/horn-ground-pre-post.smt2
@@ -0,0 +1,14 @@
+; COMMAND-LINE: --sygus-inference
+; EXPECT: sat
+(set-logic UFLIA)
+(set-info :status sat)
+
+(declare-fun I (Int Int) Bool)
+
+(assert (I 1 0))
+
+(assert (forall ((x Int) (y Int) (xp Int) (yp Int)) (=> (and (I x y) (= xp (+ x 1)) (= yp y)) (I xp yp))))
+
+(assert (not (I 1 1)))
+
+(check-sat)