}
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 ++;
}
}
* 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);
//d_bv.check(effort);
} catch(const theory::Interrupted&) {
Debug("theory") << "TheoryEngine::check() => conflict" << std::endl;
+ ok = false;
}
+ return ok;
}
/**
--- /dev/null
+(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))))
expr/node_black \
expr/kind_black \
expr/node_builder_black \
+ expr/attribute_black \
parser/parser_black \
context/context_black \
context/context_mm_black \
--- /dev/null
+/********************* */
+/** 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 <cxxtest/TestSuite.h>
+
+//Used in some of the tests
+#include <vector>
+#include <sstream>
+
+#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<MyDataAttributeId, MyData*, MyDataCleanupFunction> 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;
projects / cvc5.git / commitdiff