summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/run-script-smtcomp20176
-rw-r--r--src/smt/smt_engine.cpp1
-rw-r--r--src/theory/bv/aig_bitblaster.cpp18
-rw-r--r--src/theory/bv/bv_subtheory_core.cpp3
-rw-r--r--test/regress/regress0/quantifiers/Makefile.am5
-rw-r--r--test/regress/regress0/quantifiers/psyco-001-bv.smt276
-rw-r--r--test/regress/regress0/quantifiers/qbv-simp.smt29
7 files changed, 100 insertions, 18 deletions
diff --git a/contrib/run-script-smtcomp2017 b/contrib/run-script-smtcomp2017
index 9af6fffd0..1a9f2400f 100644
--- a/contrib/run-script-smtcomp2017
+++ b/contrib/run-script-smtcomp2017
@@ -85,19 +85,19 @@ BV|UFBV)
# many problems in UFBV are essentially BV
trywith 300 --full-saturate-quant
trywith 300 --finite-model-find
- finishwith --full-saturate-quant --decision=internal
+ finishwith --full-saturate-quant --cbqi --decision=internal
;;
LIA|LRA)
trywith 30 --full-saturate-quant
trywith 300 --full-saturate-quant --cbqi-midpoint
trywith 300 --full-saturate-quant --cbqi-nested-qe
- finishwith --full-saturate-quant --cbqi-nested-qe --decision=internal
+ finishwith --full-saturate-quant --cbqi --cbqi-nested-qe --decision=internal
;;
NIA|NRA)
trywith 30 --full-saturate-quant
trywith 300 --full-saturate-quant --nl-ext
trywith 300 --full-saturate-quant --cbqi-nested-qe
- finishwith --full-saturate-quant --cbqi-nested-qe --decision=internal
+ finishwith --full-saturate-quant --cbqi --cbqi-nested-qe --decision=internal
;;
QF_AUFBV)
trywith 600
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ace33a164..aba4f3ffc 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1855,6 +1855,7 @@ void SmtEngine::setDefaults() {
if( d_logic.isQuantified() &&
( ( options::decisionMode()!=decision::DECISION_STRATEGY_INTERNAL &&
( d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isTheoryEnabled(THEORY_DATATYPES) || d_logic.isTheoryEnabled(THEORY_BV) ) ) ||
+ d_logic.isPure(THEORY_ARITH) || d_logic.isPure(THEORY_BV) ||
options::cbqiAll() ) ){
if( !options::cbqi.wasSetByUser() ){
options::cbqi.set( true );
diff --git a/src/theory/bv/aig_bitblaster.cpp b/src/theory/bv/aig_bitblaster.cpp
index 934e2fffd..a726a0fcd 100644
--- a/src/theory/bv/aig_bitblaster.cpp
+++ b/src/theory/bv/aig_bitblaster.cpp
@@ -232,12 +232,6 @@ Abc_Obj_t* AigBitblaster::bbFormula(TNode node) {
result = node.getConst<bool>() ? mkTrue<Abc_Obj_t*>() : mkFalse<Abc_Obj_t*>();
break;
}
- case kind::VARIABLE:
- case kind::SKOLEM:
- {
- result = mkInput(node);
- break;
- }
case kind::EQUAL:
{
if( node[0].getType().isBoolean() ){
@@ -251,8 +245,12 @@ Abc_Obj_t* AigBitblaster::bbFormula(TNode node) {
//else, continue...
}
default:
- bbAtom(node);
- result = getBBAtom(node);
+ if( isVar(node) ){
+ result = mkInput(node);
+ }else{
+ bbAtom(node);
+ result = getBBAtom(node);
+ }
}
cacheAig(node, result);
@@ -315,9 +313,7 @@ void AigBitblaster::makeVariable(TNode node, Bits& bits) {
Abc_Obj_t* AigBitblaster::mkInput(TNode input) {
Assert (!hasInput(input));
Assert(input.getKind() == kind::BITVECTOR_BITOF ||
- (input.getType().isBoolean() &&
- (input.getKind() == kind::VARIABLE ||
- input.getKind() == kind::SKOLEM)));
+ (input.getType().isBoolean() && input.isVar()));
Abc_Obj_t* aig_input = Abc_NtkCreatePi(currentAigNtk());
// d_aigCache.insert(std::make_pair(input, aig_input));
d_nodeToAigInput.insert(std::make_pair(input, aig_input));
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index c59da27f4..ccce819e6 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -238,8 +238,7 @@ void CoreSolver::buildModel() {
TNode repr = *eqcs_i;
++eqcs_i;
- if (repr.getKind() != kind::VARIABLE &&
- repr.getKind() != kind::SKOLEM &&
+ if (!repr.isVar() &&
repr.getKind() != kind::CONST_BITVECTOR &&
!d_bv->isSharedTerm(repr)) {
continue;
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index 9c31204e8..eb28efdf6 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -89,8 +89,9 @@ TESTS = \
bug749-rounding.smt2 \
RNDPRE_4_1-dd-nqe.smt2 \
mix-complete-strat.smt2 \
- cbqi-sdlx-fixpoint-3-dd.smt2
-
+ cbqi-sdlx-fixpoint-3-dd.smt2 \
+ qbv-simp.smt2 \
+ psyco-001-bv.smt2
# regression can be solved with --finite-model-find --fmf-inst-engine
# set3.smt2
diff --git a/test/regress/regress0/quantifiers/psyco-001-bv.smt2 b/test/regress/regress0/quantifiers/psyco-001-bv.smt2
new file mode 100644
index 000000000..e3428de17
--- /dev/null
+++ b/test/regress/regress0/quantifiers/psyco-001-bv.smt2
@@ -0,0 +1,76 @@
+(set-logic BV)
+(set-info :status sat)
+(declare-fun W_S1_V1 () Bool)
+(declare-fun W_S1_V2 () Bool)
+(declare-fun W_S1_V4 () Bool)
+(declare-fun R_S1_V1 () Bool)
+(declare-fun R_E1_V1 () Bool)
+(declare-fun R_E1_V3 () Bool)
+(declare-fun R_E1_V2 () Bool)
+(declare-fun R_E1_V4 () Bool)
+(declare-fun DISJ_W_S1_R_E1 () Bool)
+(declare-fun R_S1_V3 () Bool)
+(declare-fun R_S1_V2 () Bool)
+(declare-fun R_S1_V4 () Bool)
+(declare-fun DISJ_W_S1_R_S1 () Bool)
+(declare-fun W_S1_V3 () Bool)
+(assert
+ (let
+ (($x324
+ (forall
+ ((V4_0 (_ BitVec 32)) (V2_0 (_ BitVec 32))
+ (V3_0 (_ BitVec 32)) (V1_0 (_ BitVec 32))
+ (MW_S1_V4 Bool) (MW_S1_V2 Bool)
+ (MW_S1_V3 Bool) (MW_S1_V1 Bool)
+ (S1_V3_!14 (_ BitVec 32)) (S1_V3_!20 (_ BitVec 32))
+ (E1_!11 (_ BitVec 32)) (E1_!16 (_ BitVec 32))
+ (E1_!17 (_ BitVec 32)) (S1_V1_!15 (_ BitVec 32))
+ (S1_V1_!21 (_ BitVec 32)) (S1_V2_!13 (_ BitVec 32))
+ (S1_V2_!19 (_ BitVec 32)) (S1_V4_!12 (_ BitVec 32))
+ (S1_V4_!18 (_ BitVec 32)))
+ (let
+ (($x267
+ (and (= (ite MW_S1_V4 S1_V4_!12 V4_0) (ite MW_S1_V4 S1_V4_!18 V4_0))
+ (= E1_!16 (ite MW_S1_V1 S1_V1_!21 E1_!17))
+ (= (ite MW_S1_V3 S1_V3_!14 V3_0) (ite MW_S1_V3 S1_V3_!20 V3_0))
+ (= (ite MW_S1_V1 S1_V1_!15 E1_!11) (ite MW_S1_V1 S1_V1_!21 E1_!17)))))
+ (let
+ (($x297
+ (and (or (not R_E1_V4) (= (ite MW_S1_V4 S1_V4_!12 V4_0) V4_0))
+ (or (not R_E1_V2) (= (ite MW_S1_V2 S1_V2_!13 V2_0) V2_0))
+ (or (not R_E1_V3) (= (ite MW_S1_V3 S1_V3_!14 V3_0) V3_0))
+ (or (not R_E1_V1) (= (ite MW_S1_V1 S1_V1_!15 E1_!11) V1_0)))))
+ (let
+ (($x310
+ (and (or (not R_E1_V4) (= V4_0 (ite MW_S1_V4 S1_V4_!12 V4_0)))
+ (or (not R_E1_V2) (= V2_0 (ite MW_S1_V2 S1_V2_!13 V2_0)))
+ (or (not R_E1_V3) (= V3_0 (ite MW_S1_V3 S1_V3_!14 V3_0)))
+ (or (not R_E1_V1) (= V1_0 (ite MW_S1_V1 S1_V1_!15 E1_!11))))))
+ (let
+ (($x321
+ (and
+ (or (not (or (not R_S1_V1) (= E1_!17 E1_!11))) (= S1_V3_!20 S1_V3_!14))
+ (or (not $x310) (= E1_!11 E1_!16))
+ (= E1_!11 E1_!17) (or (not $x297) (= E1_!16 E1_!17))
+ (or (not (or (not R_S1_V1) (= E1_!17 E1_!11))) (= S1_V1_!21 S1_V1_!15))
+ (or (not (or (not R_S1_V1) (= E1_!17 E1_!11))) (= S1_V2_!19 S1_V2_!13))
+ (or (not (or (not R_S1_V1) (= E1_!17 E1_!11))) (= S1_V4_!18 S1_V4_!12))
+ (or (not MW_S1_V4) W_S1_V4)
+ (or (not MW_S1_V2) W_S1_V2)
+ (or (not MW_S1_V1) W_S1_V1))))
+ (or (not $x321) $x267))))))))
+ (let
+ (($x40
+ (or (and W_S1_V4 R_E1_V4)
+ (and W_S1_V2 R_E1_V2) R_E1_V3
+ (and W_S1_V1 R_E1_V1))))
+ (let (($x42 (= DISJ_W_S1_R_E1 (not $x40))))
+ (let
+ (($x37
+ (or (and W_S1_V4 R_S1_V4)
+ (and W_S1_V2 R_S1_V2) R_S1_V3
+ (and W_S1_V1 R_S1_V1))))
+ (let (($x39 (= DISJ_W_S1_R_S1 (not $x37)))) (and W_S1_V3 $x39 $x42 $x324)))))))
+(check-sat)
+(exit)
+
diff --git a/test/regress/regress0/quantifiers/qbv-simp.smt2 b/test/regress/regress0/quantifiers/qbv-simp.smt2
new file mode 100644
index 000000000..1f72d44e4
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-simp.smt2
@@ -0,0 +1,9 @@
+(set-logic BV)
+(set-info :status unsat)
+(assert
+ (forall
+ ((A (_ BitVec 32)) (B (_ BitVec 32)) (C (_ BitVec 32)) (D (_ BitVec 32)))
+ (or (and (= A B) (= C D)) (and (= A C) (= B D)))))
+
+(check-sat)
+
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback