From d440c5f3bea930c4f30d62858b878ab36c676312 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Sat, 2 Jun 2018 11:18:36 -0700 Subject: [PATCH] Fix BV-abstraction check to consider SKOLEM. (#2042) Further, fix a bug in the AIG bitblaster that was also uncovered with the minimized file. --- src/theory/bv/abstraction.cpp | 10 +++++----- src/theory/bv/bitblast/aig_bitblaster.cpp | 7 ++++--- src/theory/bv/bitblast/aig_bitblaster.h | 2 ++ test/regress/Makefile.tests | 1 + test/regress/regress0/bv/bv-abstr-bug2.smt2 | 7 +++++++ 5 files changed, 19 insertions(+), 8 deletions(-) create mode 100644 test/regress/regress0/bv/bv-abstr-bug2.smt2 diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp index 46ccc4c3d..f0c1d5488 100644 --- a/src/theory/bv/abstraction.cpp +++ b/src/theory/bv/abstraction.cpp @@ -276,7 +276,7 @@ Node AbstractionModule::computeSignature(TNode node) { Node AbstractionModule::getSignatureSkolem(TNode node) { - Assert(node.getKind() == kind::VARIABLE); + Assert(node.getMetaKind() == kind::metakind::VARIABLE); NodeManager* nm = NodeManager::currentNM(); unsigned bitwidth = utils::getSize(node); if (d_signatureSkolems.find(bitwidth) == d_signatureSkolems.end()) @@ -550,8 +550,9 @@ void AbstractionModule::collectArguments(TNode node, TNode signature, std::vecto if (seen.find(node)!= seen.end()) return; - if (node.getKind() == kind::VARIABLE || - node.getKind() == kind::CONST_BITVECTOR) { + if (node.getMetaKind() == kind::metakind::VARIABLE + || node.getKind() == kind::CONST_BITVECTOR) + { // a constant in the node can either map to an argument of the abstraction // or can be hard-coded and part of the abstraction if (signature.getKind() == kind::SKOLEM) { @@ -666,8 +667,7 @@ Node AbstractionModule::substituteArguments(TNode signature, TNode apply, unsign } if (signature.getNumChildren() == 0) { - Assert (signature.getKind() != kind::VARIABLE && - signature.getKind() != kind::SKOLEM); + Assert(signature.getKind() != kind::metakind::VARIABLE); seen[signature] = signature; return signature; } diff --git a/src/theory/bv/bitblast/aig_bitblaster.cpp b/src/theory/bv/bitblast/aig_bitblaster.cpp index 7e666bcbf..80930866f 100644 --- a/src/theory/bv/bitblast/aig_bitblaster.cpp +++ b/src/theory/bv/bitblast/aig_bitblaster.cpp @@ -139,7 +139,8 @@ AigBitblaster::AigBitblaster() d_nullContext(new context::Context()), d_aigCache(), d_bbAtoms(), - d_aigOutputNode(NULL) + d_aigOutputNode(NULL), + d_notify() { prop::SatSolver* solver = nullptr; switch (options::bvSatSolver()) @@ -149,8 +150,8 @@ AigBitblaster::AigBitblaster() prop::BVSatSolverInterface* minisat = prop::SatSolverFactory::createMinisat( d_nullContext.get(), smtStatisticsRegistry(), "AigBitblaster"); - MinisatEmptyNotify notify; - minisat->setNotify(¬ify); + d_notify.reset(new MinisatEmptyNotify()); + minisat->setNotify(d_notify.get()); solver = minisat; break; } diff --git a/src/theory/bv/bitblast/aig_bitblaster.h b/src/theory/bv/bitblast/aig_bitblaster.h index 30f1dd00b..dea2d0429 100644 --- a/src/theory/bv/bitblast/aig_bitblaster.h +++ b/src/theory/bv/bitblast/aig_bitblaster.h @@ -67,6 +67,8 @@ class AigBitblaster : public TBitblaster // the thing we are checking for sat Abc_Obj_t* d_aigOutputNode; + std::unique_ptr d_notify; + void addAtom(TNode atom); void simplifyAig(); void storeBBAtom(TNode atom, Abc_Obj_t* atom_bb) override; diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 0e0cee7f8..0c5920951 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -161,6 +161,7 @@ REG0_TESTS = \ regress0/bv/bug733.smt2 \ regress0/bv/bug734.smt2 \ regress0/bv/bv-abstr-bug.smt2 \ + regress0/bv/bv-abstr-bug2.smt2 \ regress0/bv/bv-int-collapse1.smt2 \ regress0/bv/bv-int-collapse2.smt2 \ regress0/bv/bv-options1.smt2 \ diff --git a/test/regress/regress0/bv/bv-abstr-bug2.smt2 b/test/regress/regress0/bv/bv-abstr-bug2.smt2 new file mode 100644 index 000000000..939439adf --- /dev/null +++ b/test/regress/regress0/bv/bv-abstr-bug2.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --solve-int-as-bv=32 --bitblast=eager +(set-logic QF_NIA) +(set-info :status sat) +(declare-fun _substvar_7_ () Bool) +(declare-fun _substvar_3_ () Int) +(assert (or _substvar_7_ (= 0 _substvar_3_))) +(check-sat) -- 2.30.2