From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 1 Jun 2018 20:10:23 +0000 (-0500)
Subject:  Use monomial sum utility to solve for quantifiers macros (#2038)
X-Git-Tag: cvc5-1.0.0~4989
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b0fd7761fc36fc53141cb1486e9cb19dd00ae5f3;p=cvc5.git

 Use monomial sum utility to solve for quantifiers macros (#2038)
---

diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp
index 9a6cc6e97..a90227577 100644
--- a/src/theory/quantifiers/macros.cpp
+++ b/src/theory/quantifiers/macros.cpp
@@ -23,9 +23,10 @@
 #include "proof/proof_manager.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
+#include "theory/arith/arith_msum.h"
+#include "theory/quantifiers/ematching/trigger.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers/ematching/trigger.h"
 #include "theory/rewriter.h"
 
 using namespace CVC4;
@@ -218,41 +219,15 @@ Node QuantifierMacros::solveInEquality( Node n, Node lit ){
         return lit[i==0 ? 1 : 0].negate();
       }
     }
-    //must solve for term n in the literal lit
-    if( lit[0].getType().isInteger() || lit[0].getType().isReal() ){
-      Node coeff;
-      Node term;
-      //could be solved for on LHS
-      if( lit[0].getKind()==MULT && lit[0][1]==n ){
-        Assert( lit[0][0].isConst() );
-        term = lit[1];
-        coeff = lit[0][0];
-      }else{
-        Assert( lit[1].getKind()==PLUS );
-        std::vector< Node > plus_children;
-        //find monomial with n
-        for( size_t j=0; j<lit[1].getNumChildren(); j++ ){
-          if( lit[1][j]==n ){
-            Assert( coeff.isNull() );
-            coeff = NodeManager::currentNM()->mkConst( Rational(1) );
-          }else if( lit[1][j].getKind()==MULT && lit[1][j][1]==n ){
-            Assert( coeff.isNull() );
-            Assert( lit[1][j][0].isConst() );
-            coeff = lit[1][j][0];
-          }else{
-            plus_children.push_back( lit[1][j] );
-          }
-        }
-        if( !coeff.isNull() ){
-          term = plus_children.size()==1 ? plus_children[0] : NodeManager::currentNM()->mkNode( PLUS, plus_children );
-          term = NodeManager::currentNM()->mkNode( MINUS, lit[0], term );
-        }
-      }
-      if( !coeff.isNull() ){
-        coeff = NodeManager::currentNM()->mkConst( Rational(1) / coeff.getConst<Rational>() );
-        term = NodeManager::currentNM()->mkNode( MULT, coeff, term );
-        term = Rewriter::rewrite( term );
-        return term;
+    std::map<Node, Node> msum;
+    if (ArithMSum::getMonomialSumLit(lit, msum))
+    {
+      Node veq_c;
+      Node val;
+      int res = ArithMSum::isolate(n, msum, veq_c, val, EQUAL);
+      if (res != 0 && veq_c.isNull())
+      {
+        return val;
       }
     }
   }
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index b92acab94..72bb8e1d1 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -604,6 +604,7 @@ REG0_TESTS = \
 	regress0/quantifiers/lra-triv-gn.smt2 \
 	regress0/quantifiers/macros-int-real.smt2 \
 	regress0/quantifiers/macros-real-arg.smt2 \
+	regress0/quantifiers/issue2033-macro-arith.smt2 \
 	regress0/quantifiers/matching-lia-1arg.smt2 \
 	regress0/quantifiers/mix-complete-strat.smt2 \
 	regress0/quantifiers/mix-match.smt2 \
diff --git a/test/regress/regress0/quantifiers/issue2033-macro-arith.smt2 b/test/regress/regress0/quantifiers/issue2033-macro-arith.smt2
new file mode 100644
index 000000000..7993910fd
--- /dev/null
+++ b/test/regress/regress0/quantifiers/issue2033-macro-arith.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --macros-quant
+; EXPECT: sat
+(set-logic AUFNIRA)
+(set-info :status sat)
+(declare-fun _substvar_4_ () Real)
+(declare-sort S2 0)
+(declare-sort S10 0)
+(declare-fun f22 (S10 S2) Real)
+(assert (forall ((?v0 S10) (?v1 S2)) (= _substvar_4_ (- (f22 ?v0 ?v1)))))
+(check-sat)