From b260533f7b2c5fc217fa0f5036ab121249829bd4 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sun, 29 Apr 2018 22:05:53 -0500 Subject: [PATCH] Make factoring inference more aggressive (#1825) --- src/theory/arith/nonlinear_extension.cpp | 38 ++++++++++++++-------- test/regress/Makefile.tests | 2 ++ test/regress/regress1/nl/factor_agg_s.smt2 | 10 ++++++ test/regress/regress1/nl/nl_uf_lalt.smt2 | 9 +++++ 4 files changed, 45 insertions(+), 14 deletions(-) create mode 100644 test/regress/regress1/nl/factor_agg_s.smt2 create mode 100644 test/regress/regress1/nl/nl_uf_lalt.smt2 diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp index e4f35dd4c..a04d39481 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nonlinear_extension.cpp @@ -1278,12 +1278,14 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, Node shift_lem = nm->mkNode( AND, mkValidPhase(y, d_pi), - a[0].eqNode(nm->mkNode( - PLUS, - y, - nm->mkNode(MULT, nm->mkConst(Rational(2)), shift, d_pi))), - // particular case of above for shift=0 - nm->mkNode(IMPLIES, mkValidPhase(a[0], d_pi), a[0].eqNode(y)), + nm->mkNode( + ITE, + mkValidPhase(a[0], d_pi), + a[0].eqNode(y), + a[0].eqNode(nm->mkNode( + PLUS, + y, + nm->mkNode(MULT, nm->mkConst(Rational(2)), shift, d_pi)))), new_a.eqNode(a)); // must do preprocess on this one Trace("nl-ext-lemma") @@ -2748,22 +2750,30 @@ std::vector NonlinearExtension::checkFactoring( factor_to_mono_orig[itm->first[i]].push_back( itm->first ); } } - } /* else{ - factor_to_mono[itm->first].push_back( itm->second.isNull() ? d_one : itm->second ); - factor_to_mono_orig[itm->first].push_back( itm->first ); - }*/ + } } } for( std::map< Node, std::vector< Node > >::iterator itf = factor_to_mono.begin(); itf != factor_to_mono.end(); ++itf ){ + Node x = itf->first; + if (itf->second.size() == 1) + { + std::map::iterator itm = msum.find(x); + if (itm != msum.end()) + { + itf->second.push_back(itm->second.isNull() ? d_one : itm->second); + factor_to_mono_orig[x].push_back(x); + } + } if( itf->second.size()>1 ){ Node sum = NodeManager::currentNM()->mkNode(PLUS, itf->second); sum = Rewriter::rewrite( sum ); - Trace("nl-ext-factor") << "* Factored sum for " << itf->first << " : " << sum << std::endl; + Trace("nl-ext-factor") + << "* Factored sum for " << x << " : " << sum << std::endl; Node kf = getFactorSkolem( sum, lemmas ); std::vector< Node > poly; - poly.push_back( - NodeManager::currentNM()->mkNode(MULT, itf->first, kf)); - std::map< Node, std::vector< Node > >::iterator itfo = factor_to_mono_orig.find( itf->first ); + poly.push_back(NodeManager::currentNM()->mkNode(MULT, x, kf)); + std::map >::iterator itfo = + factor_to_mono_orig.find(x); Assert( itfo!=factor_to_mono_orig.end() ); for( std::map::iterator itm = msum.begin(); itm != msum.end(); ++itm ){ if( std::find( itfo->second.begin(), itfo->second.end(), itm->first )==itfo->second.end() ){ diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 5b12c005c..1ec6323b2 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1117,6 +1117,7 @@ REG1_TESTS = \ regress1/nl/exp-4.5-lt.smt2 \ regress1/nl/exp1-lb.smt2 \ regress1/nl/exp_monotone.smt2 \ + regress1/nl/factor_agg_s.smt2 \ regress1/nl/metitarski-1025.smt2 \ regress1/nl/metitarski-3-4.smt2 \ regress1/nl/metitarski_3_4_2e.smt2 \ @@ -1124,6 +1125,7 @@ REG1_TESTS = \ regress1/nl/nl-eq-infer.smt2 \ regress1/nl/nl-help-unsat-quant.smt2 \ regress1/nl/nl-unk-quant.smt2 \ + regress1/nl/nl_uf_lalt.smt2 \ regress1/nl/ones.smt2 \ regress1/nl/poly-1025.smt2 \ regress1/nl/quant-nl.smt2 \ diff --git a/test/regress/regress1/nl/factor_agg_s.smt2 b/test/regress/regress1/nl/factor_agg_s.smt2 new file mode 100644 index 000000000..4497f4c29 --- /dev/null +++ b/test/regress/regress1/nl/factor_agg_s.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --decision=justification --no-check-models +; EXPECT: sat +(set-logic QF_NRA) +(set-info :status sat) +(declare-fun skoX () Real) +(declare-fun skoY () Real) +(declare-fun skoZ () Real) +(assert (let ((?v_2 (<= 0 skoY)) (?v_0 (* skoX (- 1)))) (let ((?v_3 (* skoZ (+ 1 (* skoY ?v_0)))) (?v_4 (<= (* skoZ (+ (- 1) (* skoY skoX))) (+ skoX skoY)))) (let ((?v_1 (not ?v_4)) (?v_5 (* skoX ?v_0))) (let ((?v_6 (* skoY (* skoX (+ (- 3) ?v_5))))) (and (<= ?v_3 (+ ?v_0 (* skoY (- 1)))) (and ?v_1 (and (or ?v_1 ?v_2) (and (or ?v_2 (<= ?v_3 (+ (+ 1 ?v_0) (* skoY (+ (- 1) ?v_0))))) (and (or (not ?v_2) (or ?v_4 (<= (* skoZ (+ (+ 3 (* skoX skoX)) ?v_6)) (+ (* skoX ?v_5) (* skoY (+ (* skoX (* skoX (- 3))) ?v_6)))))) (and (not (<= skoZ 0)) (and (not (<= skoX (- 1))) (and (not (<= 1 skoY)) (not (<= skoY skoX))))))))))))))) +(check-sat) +(exit) diff --git a/test/regress/regress1/nl/nl_uf_lalt.smt2 b/test/regress/regress1/nl/nl_uf_lalt.smt2 new file mode 100644 index 000000000..5e8987d5b --- /dev/null +++ b/test/regress/regress1/nl/nl_uf_lalt.smt2 @@ -0,0 +1,9 @@ +(set-logic QF_UFNIA) +(set-info :status unsat) +(declare-fun c (Int) Int) +(declare-fun a (Int) Int) +(declare-fun b (Int) Int) +(assert (> (a 0) 0)) +(assert (= (c 0) (* (a 0) (b 0)))) +(assert (not (= (b 0) (div (c 0) (a 0))))) +(check-sat) -- 2.30.2