From 73a60e60a6036f635e8819c672c227156b351964 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 31 May 2017 15:51:35 -0500 Subject: [PATCH] Fix model construction for BV with cbqi. Minor change to defaults. --- contrib/run-script-smtcomp2017 | 6 +- src/smt/smt_engine.cpp | 1 + src/theory/bv/aig_bitblaster.cpp | 18 ++--- src/theory/bv/bv_subtheory_core.cpp | 3 +- test/regress/regress0/quantifiers/Makefile.am | 5 +- .../regress0/quantifiers/psyco-001-bv.smt2 | 76 +++++++++++++++++++ .../regress0/quantifiers/qbv-simp.smt2 | 9 +++ 7 files changed, 100 insertions(+), 18 deletions(-) create mode 100644 test/regress/regress0/quantifiers/psyco-001-bv.smt2 create mode 100644 test/regress/regress0/quantifiers/qbv-simp.smt2 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() ? mkTrue() : mkFalse(); 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) + -- 2.30.2