From 856567b63c56b238db8a5bb84ad0da7990c1f1eb Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Fri, 12 Mar 2010 23:41:12 +0000 Subject: [PATCH] Fixing unnecessary construction of NOT nodes when generating conflict clauses and: * adding the smallest test case (eq_diamond23.smt) that memouts in 50s * adding the initial attributes black box test --- src/prop/sat.h | 20 +++--- src/theory/theory_engine.h | 5 +- test/regress/regress0/uf/eq_diamond23.smt | 59 ++++++++++++++++ test/unit/Makefile.am | 1 + test/unit/expr/attribute_black.h | 86 +++++++++++++++++++++++ 5 files changed, 158 insertions(+), 13 deletions(-) create mode 100644 test/regress/regress0/uf/eq_diamond23.smt create mode 100644 test/unit/expr/attribute_black.h diff --git a/src/prop/sat.h b/src/prop/sat.h index f29436b97..7844008e8 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -174,23 +174,19 @@ SatVariable SatSolver::newVar(bool theoryAtom) { } void SatSolver::theoryCheck(SatClause& conflict) { - // Run the thoery checks - d_theoryEngine->check(theory::Theory::FULL_EFFORT); - // Try to get the conflict - Node conflictNode = d_theoryEngine->getConflict(); - // If the conflict is there, construct the conflict clause - if (!conflictNode.isNull()) { + // Try theory propagation + if (!d_theoryEngine->check(theory::Theory::FULL_EFFORT)) { + // We have a conflict, get it + Node conflictNode = d_theoryEngine->getConflict(); Debug("prop") << "SatSolver::theoryCheck() => conflict: " << conflictNode << std::endl; + // Go through the literals and construct the conflict clause Node::const_iterator literal_it = conflictNode.begin(); Node::const_iterator literal_end = conflictNode.end(); while (literal_it != literal_end) { - // Get the node and construct it's negation - Node literalNode = (*literal_it); - Node negated = literalNode.getKind() == kind::NOT ? literalNode[0] : literalNode.notNode(); // Get the literal corresponding to the node - SatLiteral l = d_cnfStream->getLiteral(negated); - // Add to the conflict clause and continue - conflict.push(l); + SatLiteral l = d_cnfStream->getLiteral(*literal_it); + // Add the negation to the conflict clause and continue + conflict.push(~l); literal_it ++; } } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 0b1afe748..cb0158dfe 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -254,7 +254,8 @@ public: * Check all (currently-active) theories for conflicts. * @param effort the effort level to use */ - inline void check(theory::Theory::Effort effort) { + inline bool check(theory::Theory::Effort effort) { + bool ok = true; try { //d_bool.check(effort); d_uf.check(effort); @@ -263,7 +264,9 @@ public: //d_bv.check(effort); } catch(const theory::Interrupted&) { Debug("theory") << "TheoryEngine::check() => conflict" << std::endl; + ok = false; } + return ok; } /** diff --git a/test/regress/regress0/uf/eq_diamond23.smt b/test/regress/regress0/uf/eq_diamond23.smt new file mode 100644 index 000000000..da00ca2ee --- /dev/null +++ b/test/regress/regress0/uf/eq_diamond23.smt @@ -0,0 +1,59 @@ +(benchmark eq_diamond23 +:source{ +Generating minimum transitivity constraints in P-time for deciding Equality Logic, +Ofer Strichman and Mirron Rozanov, +SMT Workshop 2005. + +Translator: Leonardo de Moura. } +:status unsat +:category { crafted } +:logic QF_UF +:difficulty { 2 } +:extrafuns ((x0 U) (y0 U) (z0 U) +(x1 U) (y1 U) (z1 U) +(x2 U) (y2 U) (z2 U) +(x3 U) (y3 U) (z3 U) +(x4 U) (y4 U) (z4 U) +(x5 U) (y5 U) (z5 U) +(x6 U) (y6 U) (z6 U) +(x7 U) (y7 U) (z7 U) +(x8 U) (y8 U) (z8 U) +(x9 U) (y9 U) (z9 U) +(x10 U) (y10 U) (z10 U) +(x11 U) (y11 U) (z11 U) +(x12 U) (y12 U) (z12 U) +(x13 U) (y13 U) (z13 U) +(x14 U) (y14 U) (z14 U) +(x15 U) (y15 U) (z15 U) +(x16 U) (y16 U) (z16 U) +(x17 U) (y17 U) (z17 U) +(x18 U) (y18 U) (z18 U) +(x19 U) (y19 U) (z19 U) +(x20 U) (y20 U) (z20 U) +(x21 U) (y21 U) (z21 U) +(x22 U) (y22 U) (z22 U) +) +:formula (and +(or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1))) +(or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2))) +(or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3))) +(or (and (= x3 y3) (= y3 x4)) (and (= x3 z3) (= z3 x4))) +(or (and (= x4 y4) (= y4 x5)) (and (= x4 z4) (= z4 x5))) +(or (and (= x5 y5) (= y5 x6)) (and (= x5 z5) (= z5 x6))) +(or (and (= x6 y6) (= y6 x7)) (and (= x6 z6) (= z6 x7))) +(or (and (= x7 y7) (= y7 x8)) (and (= x7 z7) (= z7 x8))) +(or (and (= x8 y8) (= y8 x9)) (and (= x8 z8) (= z8 x9))) +(or (and (= x9 y9) (= y9 x10)) (and (= x9 z9) (= z9 x10))) +(or (and (= x10 y10) (= y10 x11)) (and (= x10 z10) (= z10 x11))) +(or (and (= x11 y11) (= y11 x12)) (and (= x11 z11) (= z11 x12))) +(or (and (= x12 y12) (= y12 x13)) (and (= x12 z12) (= z12 x13))) +(or (and (= x13 y13) (= y13 x14)) (and (= x13 z13) (= z13 x14))) +(or (and (= x14 y14) (= y14 x15)) (and (= x14 z14) (= z14 x15))) +(or (and (= x15 y15) (= y15 x16)) (and (= x15 z15) (= z15 x16))) +(or (and (= x16 y16) (= y16 x17)) (and (= x16 z16) (= z16 x17))) +(or (and (= x17 y17) (= y17 x18)) (and (= x17 z17) (= z17 x18))) +(or (and (= x18 y18) (= y18 x19)) (and (= x18 z18) (= z18 x19))) +(or (and (= x19 y19) (= y19 x20)) (and (= x19 z19) (= z19 x20))) +(or (and (= x20 y20) (= y20 x21)) (and (= x20 z20) (= z20 x21))) +(or (and (= x21 y21) (= y21 x22)) (and (= x21 z21) (= z21 x22))) +(not (= x0 x22)))) diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 9d1a2995b..305731f5b 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -4,6 +4,7 @@ UNIT_TESTS = \ expr/node_black \ expr/kind_black \ expr/node_builder_black \ + expr/attribute_black \ parser/parser_black \ context/context_black \ context/context_mm_black \ diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h new file mode 100644 index 000000000..b5e897e89 --- /dev/null +++ b/test/unit/expr/attribute_black.h @@ -0,0 +1,86 @@ +/********************* */ +/** node_black.h + ** Original author: mdeters + ** Major contributors: taking + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** Black box testing of CVC4::Node. + **/ + +#include + +//Used in some of the tests +#include +#include + +#include "expr/expr_manager.h" +#include "expr/node_value.h" +#include "expr/node_builder.h" +#include "expr/node_manager.h" +#include "expr/node.h" +#include "expr/attribute.h" + +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace std; + +class AttributeBlack : public CxxTest::TestSuite { +private: + + Context* d_ctxt; + NodeManager* d_nodeManager; + NodeManagerScope* d_scope; + +public: + + void setUp() { + d_ctxt = new Context; + d_nodeManager = new NodeManager(d_ctxt); + d_scope = new NodeManagerScope(d_nodeManager); + } + + void tearDown() { + delete d_scope; + delete d_nodeManager; + delete d_ctxt; + } + + class MyData { + public: + static int count; + MyData() { count ++; } + ~MyData() { count --; } + }; + + struct MyDataAttributeId {}; + + struct MyDataCleanupFunction { + static void cleanup(MyData*& myData){ + delete myData; + } + }; + + typedef expr::Attribute MyDataAttribute; + + void testDeallocation() { + Node* node = new Node(d_nodeManager->mkVar()); + MyData* data; + MyData* data1; + MyDataAttribute attr; + TS_ASSERT(!node->hasAttribute(attr, data)); + node->setAttribute(attr, new MyData()); + TS_ASSERT(node->hasAttribute(attr, data1)); + TS_ASSERT(MyData::count == 1); + delete node; + } + +}; + +int AttributeBlack::MyData::count = 0; -- 2.30.2