From: Tim King Date: Fri, 26 May 2017 21:51:27 +0000 (-0700) Subject: Checking that equalities belong to the arithmetic theory in the solve() routine. X-Git-Tag: cvc5-1.0.0~5789 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5b2d5430d08ae663d086d8d8e3944e01062935ec;p=cvc5.git Checking that equalities belong to the arithmetic theory in the solve() routine. --- diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp index f8de2f239..14607f4e4 100644 --- a/src/theory/arith/normal_form.cpp +++ b/src/theory/arith/normal_form.cpp @@ -14,11 +14,11 @@ ** [[ Add lengthier description here ]] ** \todo document this file **/ +#include "theory/arith/normal_form.h" #include #include "base/output.h" -#include "theory/arith/normal_form.h" #include "theory/arith/arith_utilities.h" #include "theory/theory.h" @@ -805,6 +805,7 @@ DeltaRational Comparison::normalizedDeltaRational() const { } Comparison Comparison::parseNormalForm(TNode n) { + Debug("polynomial") << "Comparison::parseNormalForm(" << n << ")"; Comparison result(n); Assert(result.isNormalForm()); return result; @@ -1080,8 +1081,8 @@ bool Comparison::isNormalEqualityOrDisequality() const { /** This must be (= qvarlist qpolynomial) or (= zmonomial zpolynomial)*/ bool Comparison::isNormalEquality() const { Assert(getNode().getKind() == kind::EQUAL); - - return isNormalEqualityOrDisequality(); + return Theory::theoryOf(getNode()[0].getType()) == THEORY_ARITH && + isNormalEqualityOrDisequality(); } /** @@ -1092,7 +1093,8 @@ bool Comparison::isNormalDistinct() const { Assert(getNode().getKind() == kind::NOT); Assert(getNode()[0].getKind() == kind::EQUAL); - return isNormalEqualityOrDisequality(); + return Theory::theoryOf(getNode()[0][0].getType()) == THEORY_ARITH && + isNormalEqualityOrDisequality(); } Node Comparison::mkRatEquality(const Polynomial& p){ diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index dfe092aa5..1b97dceb2 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -1387,7 +1387,8 @@ Theory::PPAssertStatus TheoryArithPrivate::ppAssert(TNode in, SubstitutionMap& o Rational minConstant = 0; Node minMonomial; Node minVar; - if (in.getKind() == kind::EQUAL) { + if (in.getKind() == kind::EQUAL && + Theory::theoryOf(in[0].getType()) == THEORY_ARITH) { Comparison cmp = Comparison::parseNormalForm(in); Polynomial left = cmp.getLeft(); diff --git a/test/regress/regress0/uflra/Makefile.am b/test/regress/regress0/uflra/Makefile.am index 09c012ffa..78bb67bcb 100644 --- a/test/regress/regress0/uflra/Makefile.am +++ b/test/regress/regress0/uflra/Makefile.am @@ -42,7 +42,8 @@ SMT_TESTS = \ fuzz01.smt # Regression tests for SMT2 inputs -SMT2_TESTS = +SMT2_TESTS = \ + bug800.smt2 # Regression tests for PL inputs CVC_TESTS = diff --git a/test/regress/regress0/uflra/bug800.smt2 b/test/regress/regress0/uflra/bug800.smt2 new file mode 100644 index 000000000..d36f62b16 --- /dev/null +++ b/test/regress/regress0/uflra/bug800.smt2 @@ -0,0 +1,168 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +(set-logic QF_UFLRA) +(set-info :source |CPAchecker with bounded model checking on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|) +(set-info :smt-lib-version 2.0) +(set-info :category "industrial") + + +(declare-fun |__ADDRESS_OF_main::c1| () Real) +(declare-fun |__ADDRESS_OF_main::x1| () Real) +(declare-fun |__ADDRESS_OF_main::x2| () Real) +(declare-fun |__ADDRESS_OF_main::c2| () Real) +(declare-fun |main::x3@3| () Real) +(declare-fun |main::x1@3| () Real) +(declare-fun |__ADDRESS_OF_main::d3| () Real) +(declare-fun __BASE_ADDRESS_OF__ (Real) Real) +(declare-fun |main::x2@3| () Real) +(declare-fun |main::d3@2| () Real) +(declare-fun |__VERIFIER_assert::cond@2| () Real) +(declare-fun |__ADDRESS_OF_main::x3| () Real) +(declare-fun |main::d1@2| () Real) +(declare-fun |__ADDRESS_OF_main::d2| () Real) +(declare-fun |__ADDRESS_OF_main::__CPAchecker_TMP_0| () Real) +(declare-fun |main::__CPAchecker_TMP_0@3| () Real) +(declare-fun |__ADDRESS_OF_main::d1| () Real) +(declare-fun |main::d2@2| () Real) +(define-fun _7 () Real 0) +(define-fun _8 () Real |__ADDRESS_OF_main::x1|) +(define-fun _9 () Real (__BASE_ADDRESS_OF__ _8)) +(define-fun _10 () Bool (= _8 _9)) +(define-fun _11 () Real |__ADDRESS_OF_main::x2|) +(define-fun _12 () Real (__BASE_ADDRESS_OF__ _11)) +(define-fun _13 () Bool (= _11 _12)) +(define-fun _14 () Bool (and _10 _13)) +(define-fun _15 () Real |__ADDRESS_OF_main::x3|) +(define-fun _16 () Real (__BASE_ADDRESS_OF__ _15)) +(define-fun _17 () Bool (= _15 _16)) +(define-fun _18 () Bool (and _14 _17)) +(define-fun _19 () Real |__ADDRESS_OF_main::d1|) +(define-fun _20 () Real (__BASE_ADDRESS_OF__ _19)) +(define-fun _21 () Bool (= _19 _20)) +(define-fun _22 () Real 1) +(define-fun _23 () Real |main::d1@2|) +(define-fun _24 () Bool (= _23 _22)) +(define-fun _25 () Bool (and _21 _24)) +(define-fun _26 () Bool (and _18 _25)) +(define-fun _27 () Real |__ADDRESS_OF_main::d2|) +(define-fun _28 () Real (__BASE_ADDRESS_OF__ _27)) +(define-fun _29 () Bool (= _27 _28)) +(define-fun _30 () Real |main::d2@2|) +(define-fun _31 () Bool (= _30 _22)) +(define-fun _32 () Bool (and _29 _31)) +(define-fun _33 () Bool (and _26 _32)) +(define-fun _34 () Real |__ADDRESS_OF_main::d3|) +(define-fun _35 () Real (__BASE_ADDRESS_OF__ _34)) +(define-fun _36 () Bool (= _34 _35)) +(define-fun _37 () Real |main::d3@2|) +(define-fun _38 () Bool (= _37 _22)) +(define-fun _39 () Bool (and _36 _38)) +(define-fun _40 () Bool (and _33 _39)) +(define-fun _41 () Real |__ADDRESS_OF_main::c1|) +(define-fun _42 () Real (__BASE_ADDRESS_OF__ _41)) +(define-fun _43 () Bool (= _41 _42)) +(define-fun _44 () Bool (and _40 _43)) +(define-fun _45 () Real |__ADDRESS_OF_main::c2|) +(define-fun _46 () Real (__BASE_ADDRESS_OF__ _45)) +(define-fun _47 () Bool (= _45 _46)) +(define-fun _48 () Bool (and _44 _47)) +(define-fun _49 () Real |main::x1@3|) +(define-fun _50 () Bool (<= _49 _7)) +(define-fun _51 () Bool (not _50)) +(define-fun _53 () Bool (and _48 _51)) +(define-fun _54 () Bool (and _48 _50)) +(define-fun _55 () Real |main::x2@3|) +(define-fun _56 () Bool (<= _55 _7)) +(define-fun _57 () Bool (not _56)) +(define-fun _59 () Bool (and _53 _57)) +(define-fun _60 () Bool (and _53 _56)) +(define-fun _61 () Bool (or _54 _60)) +(define-fun _62 () Real |main::x3@3|) +(define-fun _63 () Bool (<= _62 _7)) +(define-fun _67 () Bool (and _59 _63)) +(define-fun _68 () Bool (or _61 _67)) +(define-fun _69 () Real |__ADDRESS_OF_main::__CPAchecker_TMP_0|) +(define-fun _70 () Real (__BASE_ADDRESS_OF__ _69)) +(define-fun _71 () Bool (= _69 _70)) +(define-fun _72 () Bool (and _68 _71)) +(define-fun _73 () Bool (= _49 _7)) +(define-fun _75 () Bool (and _72 _73)) +(define-fun _76 () Bool (not _73)) +(define-fun _77 () Bool (and _72 _76)) +(define-fun _78 () Bool (= _55 _7)) +(define-fun _80 () Bool (and _77 _78)) +(define-fun _81 () Bool (not _78)) +(define-fun _82 () Bool (and _77 _81)) +(define-fun _83 () Bool (or _75 _80)) +(define-fun _84 () Bool (= _62 _7)) +(define-fun _86 () Bool (and _82 _84)) +(define-fun _87 () Bool (not _84)) +(define-fun _88 () Bool (and _82 _87)) +(define-fun _89 () Bool (or _83 _86)) +(define-fun _90 () Real |main::__CPAchecker_TMP_0@3|) +(define-fun _91 () Bool (= _90 _7)) +(define-fun _92 () Bool (and _88 _91)) +(define-fun _93 () Bool (= _90 _22)) +(define-fun _94 () Bool (and _89 _93)) +(define-fun _95 () Bool (or _92 _94)) +(define-fun _96 () Real |__VERIFIER_assert::cond@2|) +(define-fun _97 () Bool (= _90 _96)) +(define-fun _98 () Bool (and _95 _97)) +(define-fun _99 () Bool (= _96 _7)) +(define-fun _101 () Bool (and _98 _99)) +(declare-fun __ART__34@0 () Bool) +(declare-fun |main::c2@3| () Real) +(declare-fun __ART__24@0 () Bool) +(declare-fun __ART__45@0 () Bool) +(declare-fun |main::c1@3| () Real) +(declare-fun __ART__23@0 () Bool) +(declare-fun __ART__32@0 () Bool) +(declare-fun __ART__36@0 () Bool) +(declare-fun __ART__26@0 () Bool) +(declare-fun __ART__53@0 () Bool) +(declare-fun __ART__29@0 () Bool) +(define-fun _64 () Bool (not _63)) +(define-fun _108 () Real |main::c1@3|) +(define-fun _109 () Bool (= _108 _7)) +(define-fun _123 () Real |main::c2@3|) +(define-fun _124 () Bool (= _123 _7)) +(define-fun _160 () Bool __ART__23@0) +(define-fun _161 () Bool (= _51 _160)) +(define-fun _162 () Bool __ART__24@0) +(define-fun _163 () Bool (= _57 _162)) +(define-fun _164 () Bool (and _161 _163)) +(define-fun _165 () Bool __ART__26@0) +(define-fun _166 () Bool (= _64 _165)) +(define-fun _167 () Bool (and _164 _166)) +(define-fun _168 () Bool __ART__29@0) +(define-fun _169 () Bool (= _109 _168)) +(define-fun _170 () Bool (and _167 _169)) +(define-fun _171 () Bool __ART__32@0) +(define-fun _172 () Bool (= _73 _171)) +(define-fun _173 () Bool (and _170 _172)) +(define-fun _174 () Bool __ART__34@0) +(define-fun _175 () Bool (= _78 _174)) +(define-fun _176 () Bool (and _173 _175)) +(define-fun _177 () Bool __ART__36@0) +(define-fun _178 () Bool (= _84 _177)) +(define-fun _179 () Bool (and _176 _178)) +(define-fun _180 () Bool __ART__45@0) +(define-fun _181 () Bool (= _99 _180)) +(define-fun _182 () Bool (and _179 _181)) +(define-fun _183 () Bool __ART__53@0) +(define-fun _184 () Bool (= _124 _183)) +(define-fun _185 () Bool (and _182 _184)) + + +(push 1) +(assert _101) +(set-info :status sat) +(check-sat) +(push 1) +(assert _185) +(set-info :status sat) +(check-sat) +(pop 1) +(pop 1) +(exit)