diff options
| -rw-r--r-- | contrib/run-script-smtcomp2016 | 31 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 3 | ||||
| -rw-r--r-- | src/util/bitvector.h | 17 |
3 files changed, 36 insertions, 15 deletions
diff --git a/contrib/run-script-smtcomp2016 b/contrib/run-script-smtcomp2016 index 8ac8d5c1d..534e290ed 100644 --- a/contrib/run-script-smtcomp2016 +++ b/contrib/run-script-smtcomp2016 @@ -33,6 +33,14 @@ QF_LIA) # same as QF_LRA but add --pb-rewrites finishwith --enable-miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi --pb-rewrites ;; +QF_NIA) + trywith 20 + trywith 1800 --solve-int-as-bv=2 --bitblast=eager + trywith 1800 --solve-int-as-bv=4 --bitblast=eager + trywith 1800 --solve-int-as-bv=8 --bitblast=eager + trywith 1800 --solve-int-as-bv=16 --bitblast=eager + finishwith --solve-int-as-bv=32 --bitblast=eager + ;; ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA) # the following is designed for a run time of 2400s (40 min). # initial runs 1min @@ -78,14 +86,18 @@ QF_AUFBV) trywith 600 finishwith --decision=justification-stoponly ;; -QF_ABV) - finishwith --ite-simp --simp-with-care --repeat-simp + trywith 50 --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv + trywith 500 --arrays-weak-equiv + finishwith --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv + ;; +QF_UFBV) + finishwith --bitblast=eager --bv-sat-solver=cryptominisat ;; QF_BV) exec ./pcvc4 -L smt2 --no-incremental --no-checking --no-interactive --thread-stack=1024 \ --threads 2 \ - --thread0 '--unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bitblast=eager --no-bv-abstraction' \ - --thread1 '--unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bv-eq-slicer=auto ' \ + --thread0 '--unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bitblast=eager --bv-sat-solver=cryptominisat --bitblast-aig --no-bv-native-xor --no-bv-abstraction' \ + --thread1 '--unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bv-eq-slicer=auto --no-bv-abstraction' \ --no-wait-to-join \ "$bench" #trywith 10 --bv-eq-slicer=auto --decision=justification @@ -93,11 +105,18 @@ QF_BV) #trywith 600 --decision=internal --bitblast-eager #finishwith --decision=justification --decision-use-weight --decision-weight-internal=usr1 ;; +QF_AUFLIA) + finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=justification + ;; +QF_AX) + finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=internal + ;; QF_AUFNIA) finishwith --decision=justification --no-arrays-eager-index --arrays-eager-lemmas ;; -QF_AUFLIA|QF_AX) - finishwith --no-arrays-eager-index --arrays-eager-lemmas +QF_ALIA) + trywith 70 --decision=justification --arrays-weak-equiv + finishwith --decision=justification-stoponly --no-arrays-eager-index --arrays-eager-lemmas ;; *) # just run the default diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 62afbf987..e4b9023d5 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2603,8 +2603,9 @@ Node SmtEnginePrivate::intToBV(TNode n, NodeMap& cache) { case kind::CONST_RATIONAL: { Rational constant = current.getConst<Rational>(); AlwaysAssert(constant.isIntegral()); + AlwaysAssert(constant >= 0); BitVector bv(size, constant.getNumerator()); - if (bv.getValue() != constant.getNumerator()) { + if (bv.toSignedInt() != constant.getNumerator()) { throw TypeCheckingException(current.toExpr(), string("Not enough bits for constant in intToBV: ") + current.toString()); } result = nm->mkConst(bv); diff --git a/src/util/bitvector.h b/src/util/bitvector.h index a04cbb58f..4a74c1c53 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -338,6 +338,15 @@ public: return d_value; } + Integer toSignedInt() const { + // returns Integer corresponding to two's complement interpretation of bv + unsigned size = d_size; + Integer sign_bit = d_value.extractBitRange(1,size-1); + Integer val = d_value.extractBitRange(size-1, 0); + Integer res = Integer(-1) * sign_bit.multiplyByPow2(size - 1) + val; + return res; + } + /** Returns k is the integer is equal to 2^{k-1} and zero otherwise @@ -356,14 +365,6 @@ private: unsigned d_size; Integer d_value; - Integer toSignedInt() const { - // returns Integer corresponding to two's complement interpretation of bv - unsigned size = d_size; - Integer sign_bit = d_value.extractBitRange(1,size-1); - Integer val = d_value.extractBitRange(size-1, 0); - Integer res = Integer(-1) * sign_bit.multiplyByPow2(size - 1) + val; - return res; - } };/* class BitVector */ |