Makes SyGuS parsing more robust in invariant problems (#2509)

6 files changed, 115 insertions, 53 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 40166a641..ebf50283d 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -724,31 +724,39 @@ sygusCommand [std::unique_ptr<CVC4::Command>* cmd]
         PARSER_STATE->parseError("Bad syntax for inv-constraint: expected 4 "
                                  "arguments.");
       }
-      //get primed variables
-      std::vector< Expr > primed[2];
-      std::vector< Expr > all;
-      for( unsigned i=0; i<2; i++ ){
-        PARSER_STATE->getSygusPrimedVars( primed[i], i==1 );
-        all.insert( all.end(), primed[i].begin(), primed[i].end() );
-      }
-      //make relevant terms
-      for( unsigned i=0; i<4; i++ ){
+      // get variables (regular and their respective primed versions)
+      std::vector<Expr> vars, primed_vars;
+      PARSER_STATE->getSygusInvVars(terms[0].getType(), vars, primed_vars);
+      // make relevant terms; 0 -> Inv, 1 -> Pre, 2 -> Trans, 3 -> Post
+      for (unsigned i = 0; i < 4; ++i)
+      {
         Expr op = terms[i];
-        Debug("parser-sygus") << "Make inv-constraint term #" << i << " : " << op  << "..." << std::endl;
-        std::vector< Expr > children;
-        children.push_back( op );
-        if( i==2 ){
-          children.insert( children.end(), all.begin(), all.end() );
-        }else{
-          children.insert( children.end(), primed[0].begin(), primed[0].end() );
+        Debug("parser-sygus")
+            << "Make inv-constraint term #" << i << " : " << op << " with type "
+            << op.getType() << "..." << std::endl;
+        std::vector<Expr> children;
+        children.push_back(op);
+        // transition relation applied over both variable lists
+        if (i == 2)
+        {
+          children.insert(children.end(), vars.begin(), vars.end());
+          children.insert(
+              children.end(), primed_vars.begin(), primed_vars.end());
         }
-        terms[i] = EXPR_MANAGER->mkExpr( i==0 ? kind::APPLY_UF : kind::APPLY,children);
-        if( i==0 ){
-          std::vector< Expr > children2;
-          children2.push_back( op );
-          children2.insert(children2.end(), primed[1].begin(),
-                           primed[1].end());
-          terms.push_back( EXPR_MANAGER->mkExpr(kind::APPLY_UF,children2) );
+        else
+        {
+          children.insert(children.end(), vars.begin(), vars.end());
+        }
+        terms[i] = EXPR_MANAGER->mkExpr(i == 0 ? kind::APPLY_UF : kind::APPLY,
+                                        children);
+        // make application of Inv on primed variables
+        if (i == 0)
+        {
+          children.clear();
+          children.push_back(op);
+          children.insert(
+              children.end(), primed_vars.begin(), primed_vars.end());
+          terms.push_back(EXPR_MANAGER->mkExpr(kind::APPLY_UF, children));
         }
       }
       //make constraints
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index dfeaca62b..c3a107bdf 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -629,20 +629,18 @@ void Smt2::includeFile(const std::string& filename) {
   }
 }
 
-Expr Smt2::mkSygusVar(const std::string& name, const Type& type, bool isPrimed) {
-  Expr e = mkBoundVar(name, type);
-  d_sygusVars.push_back(e);
-  d_sygusVarPrimed[e] = false;
-  if( isPrimed ){
-    d_sygusInvVars.push_back(e);
-    std::stringstream ss;
-    ss << name << "'";
-    Expr ep = mkBoundVar(ss.str(), type);
-    d_sygusVars.push_back(ep);
-    d_sygusInvVars.push_back(ep);
-    d_sygusVarPrimed[ep] = true;
+void Smt2::mkSygusVar(const std::string& name, const Type& type, bool isPrimed)
+{
+  if (!isPrimed)
+  {
+    d_sygusVars.push_back(mkBoundVar(name, type));
   }
-  return e;
+#ifdef CVC4_ASSERTIONS
+  else
+  {
+    d_sygusVarPrimed.push_back(mkBoundVar(name, type));
+  }
+#endif
 }
 
 void Smt2::mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops ) {
@@ -1235,16 +1233,40 @@ Expr Smt2::makeSygusBoundVarList(Datatype& dt,
   return getExprManager()->mkExpr(kind::BOUND_VAR_LIST, lvars);
 }
 
-const void Smt2::getSygusPrimedVars( std::vector<Expr>& vars, bool isPrimed ) {
-  for (unsigned i = 0, size = d_sygusInvVars.size(); i < size; i++)
+const void Smt2::getSygusInvVars(FunctionType t,
+                                 std::vector<Expr>& vars,
+                                 std::vector<Expr>& primed_vars)
+{
+  std::vector<Type> argTypes = t.getArgTypes();
+  ExprManager* em = getExprManager();
+  for (const Type& ti : argTypes)
   {
-    Expr v = d_sygusInvVars[i];
-    std::map< Expr, bool >::iterator it = d_sygusVarPrimed.find( v );
-    if( it!=d_sygusVarPrimed.end() ){
-      if( it->second==isPrimed ){
-        vars.push_back( v );
+    vars.push_back(em->mkBoundVar(ti));
+    d_sygusVars.push_back(vars.back());
+    std::stringstream ss;
+    ss << vars.back() << "'";
+    primed_vars.push_back(em->mkBoundVar(ss.str(), ti));
+    d_sygusVars.push_back(primed_vars.back());
+#ifdef CVC4_ASSERTIONS
+    bool find_new_declared_var = false;
+    for (const Expr& e : d_sygusVarPrimed)
+    {
+      if (e.getType() == ti)
+      {
+        d_sygusVarPrimed.erase(
+            std::find(d_sygusVarPrimed.begin(), d_sygusVarPrimed.end(), e));
+        find_new_declared_var = true;
+        break;
       }
     }
+    if (!find_new_declared_var)
+    {
+      ss.str("");
+      ss << "warning: decleared primed variables do not match invariant's "
+            "type\n";
+      warning(ss.str());
+    }
+#endif
   }
 }
 
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 64a957402..80bd8df83 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -68,17 +68,16 @@ private:
   std::unordered_map<std::string, Kind> operatorKindMap;
   std::pair<Expr, std::string> d_lastNamedTerm;
   // for sygus
-  std::vector<Expr> d_sygusVars, d_sygusInvVars, d_sygusConstraints,
+  std::vector<Expr> d_sygusVars, d_sygusVarPrimed, d_sygusConstraints,
       d_sygusFunSymbols;
-  std::map< Expr, bool > d_sygusVarPrimed;
 
-protected:
- Smt2(api::Solver* solver,
-      Input* input,
-      bool strictMode = false,
-      bool parseOnly = false);
+ protected:
+  Smt2(api::Solver* solver,
+       Input* input,
+       bool strictMode = false,
+       bool parseOnly = false);
 
-public:
+ public:
   /**
    * Add theory symbols to the parser state.
    *
@@ -228,7 +227,9 @@ public:
     return getExprManager()->mkConst(AbstractValue(Integer(name.substr(1))));
   }
 
-  Expr mkSygusVar(const std::string& name, const Type& type, bool isPrimed = false);
+  void mkSygusVar(const std::string& name,
+                  const Type& type,
+                  bool isPrimed = false);
 
   void mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops );
 
@@ -287,7 +288,14 @@ public:
   const std::vector<Expr>& getSygusVars() {
     return d_sygusVars;
   }
-  const void getSygusPrimedVars( std::vector<Expr>& vars, bool isPrimed );
+  /** retrieves the invariant variables (both regular and primed)
+   *
+   * To ensure that the variable list represent the correct argument type order
+   * the type  of the invariant predicate is used during the variable retrieval
+   */
+  const void getSygusInvVars(FunctionType t,
+                             std::vector<Expr>& vars,
+                             std::vector<Expr>& primed_vars);
 
   const void addSygusFunSymbol( Type t, Expr synth_fun );
   const std::vector<Expr>& getSygusFunSymbols() {
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 35672d77a..5252954dc 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -826,6 +826,7 @@ set(regress_0_tests
   regress0/sygus/check-generic-red.sy
   regress0/sygus/const-var-test.sy
   regress0/sygus/dt-no-syntax.sy
+  regress0/sygus/inv-different-var-order.sy
   regress0/sygus/let-ringer.sy
   regress0/sygus/let-simp.sy
   regress0/sygus/no-syntax-test-bool.sy
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index c79f42078..08d0ca5bb 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -839,6 +839,7 @@ REG0_TESTS = \
 	regress0/sygus/const-var-test.sy \
 	regress0/sygus/dt-no-syntax.sy \
 	regress0/sygus/hd-05-d1-prog-nogrammar.sy \
+	regress0/sygus/inv-different-var-order.sy \
 	regress0/sygus/let-ringer.sy \
 	regress0/sygus/let-simp.sy \
 	regress0/sygus/no-syntax-test-bool.sy \
diff --git a/test/regress/regress0/sygus/inv-different-var-order.sy b/test/regress/regress0/sygus/inv-different-var-order.sy
new file mode 100644
index 000000000..c3f43fc07
--- /dev/null
+++ b/test/regress/regress0/sygus/inv-different-var-order.sy
@@ -0,0 +1,22 @@
+; COMMAND-LINE: --sygus-out=status
+;EXPECT: unsat
+(set-logic LIA)
+(synth-inv inv-f ((x Int) (y Int) (b Bool)))
+(declare-primed-var b Bool)
+(declare-primed-var x Int)
+(declare-primed-var y Int)
+(define-fun pre-f ((x Int) (y Int) (b Bool)) Bool
+(and
+(and (>= x 5) (<= x 9))
+(and (>= y 1) (<= y 3))
+)
+)
+(define-fun trans-f ((x Int) (y Int) (b Bool) (x! Int) (y! Int) (b! Bool)) Bool
+(and
+(and (= b! b) (= y! x))
+(ite b (= x! (+ x 10)) (= x! (+ x 12)))
+)
+)
+(define-fun post-f ((x Int) (y Int) (b Bool)) Bool true)
+(inv-constraint inv-f pre-f trans-f post-f)
+(check-synth)
\ No newline at end of file