Make factoring inference more aggressive (#1825)

4 files changed, 45 insertions, 14 deletions

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<Node>& 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<Node> 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<Node, Node>::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<Node, std::vector<Node> >::iterator itfo =
+                factor_to_mono_orig.find(x);
             Assert( itfo!=factor_to_mono_orig.end() );
             for( std::map<Node, Node>::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)