diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-06-01 15:10:23 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-06-01 13:10:23 -0700 |
commit | b0fd7761fc36fc53141cb1486e9cb19dd00ae5f3 (patch) | |
tree | 56da6668e0d328943b9a4906b49bafca2aed7c83 | |
parent | 4be329c881c510caab5995b5ecbe3ae9961b3eed (diff) |
Use monomial sum utility to solve for quantifiers macros (#2038)
-rw-r--r-- | src/theory/quantifiers/macros.cpp | 47 | ||||
-rw-r--r-- | test/regress/Makefile.tests | 1 | ||||
-rw-r--r-- | test/regress/regress0/quantifiers/issue2033-macro-arith.smt2 | 10 |
3 files changed, 22 insertions, 36 deletions
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) |