From c77262836774c08d5c05fb057348b820a2643c07 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 20 Dec 2017 22:26:17 -0600 Subject: [PATCH] Fixes for cbqi-bv (#1449) --- src/smt/smt_engine.cpp | 2 +- src/theory/quantifiers/ceg_t_instantiator.cpp | 96 +++++++++---------- src/theory/quantifiers/inst_strategy_cbqi.cpp | 1 - test/regress/regress0/quantifiers/Makefile.am | 3 +- .../regress0/quantifiers/model_6_1_bv.smt2 | 15 +++ 5 files changed, 64 insertions(+), 53 deletions(-) create mode 100644 test/regress/regress0/quantifiers/model_6_1_bv.smt2 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index e7736ebfc..4336b7a05 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1937,7 +1937,7 @@ void SmtEngine::setDefaults() { } }else{ // only supported in pure arithmetic or pure BV - if (d_logic.isPure(THEORY_BV)) + if (!d_logic.isPure(THEORY_BV)) { options::cbqiNestedQE.set(false); } diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp index e4bc9adb8..8a0412a80 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.cpp +++ b/src/theory/quantifiers/ceg_t_instantiator.cpp @@ -1887,66 +1887,62 @@ void BvInstantiatorPreprocess::registerCounterexampleLemma( } for (std::pair >& es : extract_map) { - if (es.second.size() > 1) - { - // sort based on the extract start position - std::vector& curr_vec = es.second; + // sort based on the extract start position + std::vector& curr_vec = es.second; - SortBvExtractInterval sbei; - std::sort(curr_vec.begin(), curr_vec.end(), sbei); + SortBvExtractInterval sbei; + std::sort(curr_vec.begin(), curr_vec.end(), sbei); - unsigned width = es.first.getType().getBitVectorSize(); + unsigned width = es.first.getType().getBitVectorSize(); - // list of points b such that: - // b>0 and we must start a segment at (b-1) or b==0 - std::vector boundaries; - boundaries.push_back(width); - boundaries.push_back(0); + // list of points b such that: + // b>0 and we must start a segment at (b-1) or b==0 + std::vector boundaries; + boundaries.push_back(width); + boundaries.push_back(0); - Trace("cegqi-bv-pp") << "For term " << es.first << " : " << std::endl; - for (unsigned i = 0, size = curr_vec.size(); i < size; i++) + Trace("cegqi-bv-pp") << "For term " << es.first << " : " << std::endl; + for (unsigned i = 0, size = curr_vec.size(); i < size; i++) + { + Trace("cegqi-bv-pp") << " " << i << " : " << curr_vec[i] << std::endl; + BitVectorExtract e = + curr_vec[i].getOperator().getConst(); + if (std::find(boundaries.begin(), boundaries.end(), e.high + 1) + == boundaries.end()) { - Trace("cegqi-bv-pp") << " " << i << " : " << curr_vec[i] - << std::endl; - BitVectorExtract e = - curr_vec[i].getOperator().getConst(); - if (std::find(boundaries.begin(), boundaries.end(), e.high + 1) - == boundaries.end()) - { - boundaries.push_back(e.high + 1); - } - if (std::find(boundaries.begin(), boundaries.end(), e.low) - == boundaries.end()) - { - boundaries.push_back(e.low); - } + boundaries.push_back(e.high + 1); } - std::sort(boundaries.rbegin(), boundaries.rend()); - - // make the extract variables - std::vector children; - for (unsigned i = 1; i < boundaries.size(); i++) + if (std::find(boundaries.begin(), boundaries.end(), e.low) + == boundaries.end()) { - Assert(boundaries[i - 1] > 0); - Node ex = bv::utils::mkExtract( - es.first, boundaries[i - 1] - 1, boundaries[i]); - Node var = - nm->mkSkolem("ek", - ex.getType(), - "variable to represent disjoint extract region"); - Node ceq_lem = var.eqNode(ex); - Trace("cegqi-bv-pp") << "Introduced : " << ceq_lem << std::endl; - new_lems.push_back(ceq_lem); - children.push_back(var); - vars.push_back(var); + boundaries.push_back(e.low); } + } + std::sort(boundaries.rbegin(), boundaries.rend()); - Node conc = nm->mkNode(kind::BITVECTOR_CONCAT, children); - Assert(conc.getType() == es.first.getType()); - Node eq_lem = conc.eqNode(es.first); - Trace("cegqi-bv-pp") << "Introduced : " << eq_lem << std::endl; - new_lems.push_back(eq_lem); + // make the extract variables + std::vector children; + for (unsigned i = 1; i < boundaries.size(); i++) + { + Assert(boundaries[i - 1] > 0); + Node ex = bv::utils::mkExtract( + es.first, boundaries[i - 1] - 1, boundaries[i]); + Node var = + nm->mkSkolem("ek", + ex.getType(), + "variable to represent disjoint extract region"); + Node ceq_lem = var.eqNode(ex); + Trace("cegqi-bv-pp") << "Introduced : " << ceq_lem << std::endl; + new_lems.push_back(ceq_lem); + children.push_back(var); + vars.push_back(var); } + + Node conc = nm->mkNode(kind::BITVECTOR_CONCAT, children); + Assert(conc.getType() == es.first.getType()); + Node eq_lem = conc.eqNode(es.first); + Trace("cegqi-bv-pp") << "Introduced : " << eq_lem << std::endl; + new_lems.push_back(eq_lem); Trace("cegqi-bv-pp") << "...finished processing extracts for term " << es.first << std::endl; } diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 668593842..bd2b8e78e 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -744,7 +744,6 @@ bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) { }else{ //this should never happen for monotonic selection strategies Trace("cbqi-warn") << "WARNING: Existing instantiation" << std::endl; - Assert( !options::cbqiNestedQE() || options::cbqiAll() ); return false; } } diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index bb43d6c1c..a8c25ae5a 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -134,7 +134,8 @@ TESTS = \ javafe.ast.WhileStmt.447.smt2 \ clock-10.smt2 \ javafe.tc.FlowInsensitiveChecks.682.smt2 \ - javafe.tc.CheckCompilationUnit.001.smt2 + javafe.tc.CheckCompilationUnit.001.smt2 \ + model_6_1_bv.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine diff --git a/test/regress/regress0/quantifiers/model_6_1_bv.smt2 b/test/regress/regress0/quantifiers/model_6_1_bv.smt2 new file mode 100644 index 000000000..011430bd6 --- /dev/null +++ b/test/regress/regress0/quantifiers/model_6_1_bv.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --cbqi-nested-qe +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun lambda () (_ BitVec 32)) +(declare-fun lambdaprime () (_ BitVec 32)) +(declare-fun x5 () (_ BitVec 32)) +(declare-fun x4 () (_ BitVec 32)) +(declare-fun bool.b22 () Bool) +(declare-fun bool.b7 () Bool) +(declare-fun bool.b5 () Bool) +(declare-fun bool.b6 () Bool) +(assert (forall ((?lambda (_ BitVec 32))) (or (or (exists ((?lambdaprime (_ BitVec 32))) (let ((?v_1 (not bool.b22)) (?v_3 (not bool.b7)) (?v_4 (not bool.b5))) (let ((?v_2 (and ?v_4 (not bool.b6))) (?v_0 (bvmul (bvneg (_ bv1 32)) (bvadd x4 (bvmul (_ bv30 32) ?lambdaprime))))) (and (and (bvsle (_ bv0 32) ?lambdaprime) (bvsle ?lambdaprime ?lambda)) (not (and (not (bvsle (bvmul (bvneg (_ bv1 32)) (bvadd x5 (bvmul (_ bv1 32) ?lambdaprime))) (bvneg (_ bv10 32)))) (and (and (not (and (bvsle ?v_0 (bvneg (_ bv4100 32))) (and ?v_1 (and ?v_3 ?v_2)))) (not (and (bvsle ?v_0 (bvneg (_ bv4500 32))) (and ?v_1 (and bool.b7 ?v_2))))) (not (and (bvsle ?v_0 (bvneg (_ bv4910 32))) (and ?v_1 (and ?v_3 (and ?v_4 bool.b6)))))))))))) (bvslt ?lambda (_ bv0 32))) (not (and (not bool.b22) (and (not bool.b7) (and bool.b5 (not bool.b6)))))))) +(check-sat) +(exit) -- 2.30.2