From 9f18a444d5c926cffa0532995a3a50cf74a98769 Mon Sep 17 00:00:00 2001 From: Tim King Date: Mon, 7 May 2012 22:06:07 +0000 Subject: [PATCH] Fixes a sign bug in the DioSolver. --- src/theory/arith/dio_solver.cpp | 9 ++++---- test/regress/regress0/arith/Makefile.am | 3 ++- test/regress/regress0/arith/problem__003.smt2 | 21 +++++++++++++++++++ 3 files changed, 28 insertions(+), 5 deletions(-) create mode 100644 test/regress/regress0/arith/problem__003.smt2 diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp index 613ce8368..28fe86c70 100644 --- a/src/theory/arith/dio_solver.cpp +++ b/src/theory/arith/dio_solver.cpp @@ -375,6 +375,7 @@ DioSolver::TrailIndex DioSolver::impliedGcdOfOne(){ //For the rest of the equations keep reducing until the coefficient is one for(; iter != end; ++iter){ + Debug("arith::dio") << "next round : " << currentCoeff << " " << currentGcd << endl; TrailIndex inQueue = *iter; Constant iqc = d_trail[inQueue].d_eq.getPolynomial().getCoefficient(vl); if(!iqc.isZero()){ @@ -385,9 +386,9 @@ DioSolver::TrailIndex DioSolver::impliedGcdOfOne(){ // g = a*s + b*t Integer::extendedGcd(g, s, t, currentCoeff, inQueueCoeff); - Debug("arith::dio") << "extendedReduction" << endl; + Debug("arith::dio") << "extendedReduction : " << endl; Debug("arith::dio") << g << " = " << s <<"*"<< currentCoeff << " + " << t <<"*"<< inQueueCoeff << endl; - + Assert(g <= currentGcd); if(g < currentGcd){ if(s.sgn() == 0){ @@ -395,10 +396,10 @@ DioSolver::TrailIndex DioSolver::impliedGcdOfOne(){ Assert(inQueueCoeff.divides(currentGcd)); current = *iter; currentCoeff = inQueueCoeff; - currentGcd = inQueueCoeff; + currentGcd = inQueueCoeff.abs(); }else{ + Debug("arith::dio") << "extendedReduction combine" << endl; - TrailIndex next = combineEqAtIndexes(current, s, inQueue, t); Assert(d_trail[next].d_eq.getPolynomial().getCoefficient(vl).getValue().getNumerator() == g); diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am index 7136662e6..28d116c4a 100644 --- a/test/regress/regress0/arith/Makefile.am +++ b/test/regress/regress0/arith/Makefile.am @@ -19,7 +19,8 @@ TESTS = \ delta-minimized-row-vector-bug.smt \ fuzz_3-eq.smt \ leq.01.smt \ - miplibtrick.smt + miplibtrick.smt \ + problem__003.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/arith/problem__003.smt2 b/test/regress/regress0/arith/problem__003.smt2 new file mode 100644 index 000000000..7af727e2a --- /dev/null +++ b/test/regress/regress0/arith/problem__003.smt2 @@ -0,0 +1,21 @@ +(set-logic QF_LIA) +(set-info :source | +Alberto Griggio + +|) +(set-info :smt-lib-version 2.0) +(set-info :category "random") +(set-info :status sat) +(declare-fun x0 () Int) +(declare-fun x1 () Int) +(declare-fun x2 () Int) +(declare-fun x3 () Int) +(declare-fun x4 () Int) +(declare-fun x5 () Int) +(declare-fun x6 () Int) +(declare-fun x7 () Int) +(declare-fun x8 () Int) +(declare-fun x9 () Int) +(assert (let ((?v_3 (* 36 x4)) (?v_0 (* 37 x7)) (?v_21 (* 3 x1)) (?v_7 (* 1 x1)) (?v_2 (* 23 x0)) (?v_4 (* 37 x1)) (?v_23 (* 15 x8)) (?v_11 (* 24 x1)) (?v_14 (* 30 x5)) (?v_17 (* 31 x6)) (?v_19 (* 28 x5)) (?v_5 (* 26 x5)) (?v_12 (* 13 x5)) (?v_20 (* 5 x6)) (?v_1 (* (- 38) x0)) (?v_18 (* (- 33) x4)) (?v_22 (* (- 38) x1)) (?v_16 (* (- 24) x6)) (?v_6 (* (- 13) x1)) (?v_9 (* (- 8) x4)) (?v_13 (* (- 11) x9)) (?v_10 (* (- 6) x0)) (?v_15 (* (- 37) x7)) (?v_8 (* (- 3) x4))) (and (<= (+ (* 25 x2) (* 12 x8) (* 12 x7) ?v_3 (* (- 5) x6) (* (- 25) x7) (* 22 x5) (* 7 x6) (* (- 19) x5) (* 22 x8)) (- 4)) (<= (+ (* 16 x1) (* 27 x2) (* 36 x6) (* 0 x8) (* 18 x4) (* (- 6) x1) (* 3 x9) (* (- 31) x9) (* 8 x0) ?v_0) (- 39)) (<= (+ (* 22 x1) (* 14 x3) (* (- 1) x2) (* (- 29) x9) (* 25 x8) (* 27 x4) (* (- 8) x3) (* (- 17) x4) ?v_1 (* 7 x7)) (- 25)) (<= (+ (* 16 x2) (* 2 x5) (* (- 34) x8) (* 3 x7) ?v_21 (* (- 17) x9) (* (- 32) x4) (* (- 7) x9) (* (- 9) x2) (* 16 x8)) (- 39)) (<= (+ ?v_7 (* (- 8) x5) (* 6 x4) ?v_18 (* (- 37) x0) (* 16 x6) (* (- 12) x0) (* 22 x3) (* (- 36) x3) (* 36 x0)) 6) (<= (+ (* 9 x3) (* (- 36) x4) (* (- 32) x8) (* (- 16) x1) ?v_0 ?v_2 (* (- 6) x5) (* (- 31) x6) (* (- 5) x8) (* (- 15) x3)) (- 15)) (<= (+ (* 1 x8) (* (- 7) x6) ?v_4 (* 20 x2) ?v_1 (* 0 x0) (* (- 37) x8) (* 13 x3) (* (- 23) x7) (* 37 x9)) (- 14)) (<= (+ (* 34 x5) (* 10 x6) (* (- 3) x5) (* (- 38) x9) ?v_22 (* 19 x6) (* (- 39) x7) ?v_16 (* 12 x1) (* (- 3) x7)) 35) (<= (+ (* 20 x4) (* (- 39) x9) (* 24 x3) ?v_23 (* (- 18) x3) ?v_11 (* (- 23) x4) ?v_14 (* 11 x2) (* (- 1) x5)) (- 13)) (<= (+ (* 30 x9) ?v_17 (* 14 x2) ?v_6 (* (- 16) x8) (* 29 x1) (* (- 3) x6) ?v_9 (* (- 10) x8) ?v_19) (- 39)) (<= (+ (* 8 x4) (* 37 x2) ?v_13 (* 23 x2) ?v_2 (* (- 4) x1) (* 10 x5) (* (- 36) x0) (* (- 15) x0) (* (- 22) x3)) (- 24)) (<= (+ (* 38 x2) (* 23 x3) (* 12 x2) ?v_10 ?v_3 (* 29 x6) (* 4 x0) ?v_5 ?v_15 (* (- 10) x9)) 16) (<= (+ (* 31 x4) (* (- 26) x0) (* (- 19) x9) (* (- 21) x4) ?v_4 ?v_8 ?v_5 ?v_12 (* (- 20) x4) (* (- 31) x2)) (- 12)) (<= (+ (* 38 x9) (* (- 28) x1) (* 29 x0) (* 5 x1) (* (- 38) x8) ?v_6 (* (- 8) x2) ?v_20 (* 22 x7) (* (- 24) x9)) 10) (<= (+ ?v_7 ?v_8 (* 35 x5) (* 16 x3) (* 6 x7) ?v_9 (* (- 2) x3) (* (- 38) x5) ?v_10 (* (- 7) x4)) (- 29)) (<= (+ (* 11 x3) (* 5 x4) (* (- 2) x4) (* 37 x6) ?v_11 (* 0 x9) (* 25 x1) (* (- 3) x9) (* (- 33) x9) (* 19 x9)) (- 37)) (<= (+ ?v_12 (* 7 x4) ?v_13 ?v_14 (* (- 31) x0) (* (- 12) x6) (* (- 35) x0) (* 36 x2) (* (- 25) x3) ?v_15) (- 33)) (<= (+ (* 10 x4) ?v_16 (* 26 x6) ?v_17 ?v_18 (* (- 32) x5) (* 32 x2) (* 34 x8) (* 19 x1) ?v_1) (- 9)) (<= (+ ?v_12 (* (- 9) x3) (* (- 37) x3) (* 34 x4) (* 0 x1) ?v_19 (* 30 x6) (* (- 18) x4) (* 21 x5) (* (- 21) x9)) (- 9)) (<= (+ ?v_20 (* (- 30) x6) ?v_21 (* 9 x8) ?v_13 (* (- 28) x5) (* (- 14) x3) ?v_22 (* 5 x8) ?v_23) 35)))) +(check-sat) +(exit) -- 2.30.2