test/unit/prop/cnf_stream_black.h

   1 /*********************                                                        */
   2 /*! \file cnf_stream_black.h
   3  ** \verbatim
   4  ** Original author: cconway
   5  ** Major contributors: mdeters
   6  ** Minor contributors (to current version): taking, dejan
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief White box testing of CVC4::prop::CnfStream.
  15  **
  16  ** White box testing of CVC4::prop::CnfStream.
  17  **/
  18
  19 #include <cxxtest/TestSuite.h>
  20 /* #include <gmock/gmock.h> */
  21 /* #include <gtest/gtest.h> */
  22
  23 #include "util/Assert.h"
  24
  25
  26 #include "expr/expr_manager.h"
  27 #include "expr/node_manager.h"
  28 #include "context/context.h"
  29 #include "prop/cnf_stream.h"
  30 #include "prop/prop_engine.h"
  31 #include "prop/theory_proxy.h"
  32 #include "smt/smt_engine.h"
  33
  34 #include "theory/theory.h"
  35 #include "theory/theory_engine.h"
  36 #include "theory/theory_registrar.h"
  37
  38 #include "theory/builtin/theory_builtin.h"
  39 #include "theory/booleans/theory_bool.h"
  40 #include "theory/arith/theory_arith.h"
  41
  42 using namespace CVC4;
  43 using namespace CVC4::context;
  44 using namespace CVC4::prop;
  45 using namespace std;
  46
  47 /* This fake class relies on the face that a MiniSat variable is just an int. */
  48 class FakeSatSolver : public SatSolver {
  49   SatVariable d_nextVar;
  50   bool d_addClauseCalled;
  51
  52 public:
  53   FakeSatSolver() :
  54     d_nextVar(0),
  55     d_addClauseCalled(false) {
  56   }
  57
  58   SatVariable newVar(bool theoryAtom) {
  59     return d_nextVar++;
  60   }
  61
  62   SatVariable trueVar() {
  63     return d_nextVar++;
  64   }
  65
  66   SatVariable falseVar() {
  67     return d_nextVar++;
  68   }
  69
  70   void addClause(SatClause& c, bool lemma) {
  71     d_addClauseCalled = true;
  72   }
  73
  74   void reset() {
  75     d_addClauseCalled = false;
  76   }
  77
  78   unsigned int addClauseCalled() {
  79     return d_addClauseCalled;
  80   }
  81
  82   unsigned getAssertionLevel() const {
  83     return 0;
  84   }
  85
  86   void unregisterVar(SatLiteral lit) {
  87   }
  88
  89   void renewVar(SatLiteral lit, int level = -1) {
  90   }
  91
  92   void interrupt() {
  93   }
  94
  95   SatValue solve() {
  96     return SAT_VALUE_UNKNOWN;
  97   }
  98
  99   SatValue solve(long unsigned int& resource) {
 100     return SAT_VALUE_UNKNOWN;
 101   }
 102
 103   SatValue value(SatLiteral l) {
 104     return SAT_VALUE_UNKNOWN;
 105   }
 106
 107   SatValue modelValue(SatLiteral l) {
 108     return SAT_VALUE_UNKNOWN;
 109   }
 110
 111   bool properExplanation(SatLiteral lit, SatLiteral expl) const {
 112     return true;
 113   }
 114
 115 };/* class FakeSatSolver */
 116
 117 class CnfStreamBlack : public CxxTest::TestSuite {
 118   /** The SAT solver proxy */
 119   FakeSatSolver* d_satSolver;
 120
 121   /** The logic info */
 122   LogicInfo* d_logicInfo;
 123
 124   /** The theory engine */
 125   TheoryEngine* d_theoryEngine;
 126
 127   /** The output channel */
 128   theory::OutputChannel* d_outputChannel;
 129
 130   /** The CNF converter in use */
 131   CnfStream* d_cnfStream;
 132
 133   /** The context */
 134   Context* d_context;
 135
 136   /** The user context */
 137   UserContext* d_userContext;
 138
 139   /** The node manager */
 140   NodeManager* d_nodeManager;
 141
 142   void setUp() {
 143     d_context = new Context();
 144     d_userContext = new UserContext();
 145     d_nodeManager = new NodeManager(d_context, NULL);
 146     NodeManagerScope nms(d_nodeManager);
 147     d_satSolver = new FakeSatSolver();
 148     d_logicInfo = new LogicInfo();
 149     d_logicInfo->lock();
 150     d_theoryEngine = new TheoryEngine(d_context, d_userContext, *d_logicInfo);
 151     d_theoryEngine->addTheory<theory::builtin::TheoryBuiltin>(theory::THEORY_BUILTIN);
 152     d_theoryEngine->addTheory<theory::booleans::TheoryBool>(theory::THEORY_BOOL);
 153     d_theoryEngine->addTheory<theory::arith::TheoryArith>(theory::THEORY_ARITH);
 154     d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, new theory::TheoryRegistrar(d_theoryEngine));
 155   }
 156
 157   void tearDown() {
 158     NodeManagerScope nms(d_nodeManager);
 159     delete d_cnfStream;
 160     d_theoryEngine->shutdown();
 161     delete d_theoryEngine;
 162     delete d_logicInfo;
 163     delete d_satSolver;
 164     delete d_nodeManager;
 165     delete d_userContext;
 166     delete d_context;
 167   }
 168
 169 public:
 170
 171   /* [chris 5/26/2010] In the tests below, we don't attempt to delve into the
 172    * deep structure of the CNF conversion. Firstly, we just want to make sure
 173    * that the conversion doesn't choke on any boolean Exprs. We'll also check
 174    * that addClause got called. We won't check that it gets called a particular
 175    * number of times, or with what.
 176    */
 177
 178   void testAnd() {
 179     NodeManagerScope nms(d_nodeManager);
 180     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
 181     Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
 182     Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
 183     d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::AND, a, b, c), false, false);
 184     TS_ASSERT( d_satSolver->addClauseCalled() );
 185   }
 186
 187   void testComplexExpr() {
 188     NodeManagerScope nms(d_nodeManager);
 189     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
 190     Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
 191     Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
 192     Node d = d_nodeManager->mkVar(d_nodeManager->booleanType());
 193     Node e = d_nodeManager->mkVar(d_nodeManager->booleanType());
 194     Node f = d_nodeManager->mkVar(d_nodeManager->booleanType());
 195     d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::IMPLIES,
 196                                                         d_nodeManager->mkNode(kind::AND, a, b),
 197                                                         d_nodeManager->mkNode(kind::IFF,
 198                                                                               d_nodeManager->mkNode(kind::OR, c, d),
 199                                                                               d_nodeManager->mkNode(kind::NOT,
 200                                                                                                     d_nodeManager->mkNode(kind::XOR, e, f)))), false, false );
 201     TS_ASSERT( d_satSolver->addClauseCalled() );
 202   }
 203
 204   void testTrue() {
 205     NodeManagerScope nms(d_nodeManager);
 206     d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true), false, false );
 207     TS_ASSERT( d_satSolver->addClauseCalled() );
 208   }
 209
 210   void testFalse() {
 211     NodeManagerScope nms(d_nodeManager);
 212     d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false), false, false );
 213     TS_ASSERT( d_satSolver->addClauseCalled() );
 214   }
 215
 216   void testIff() {
 217     NodeManagerScope nms(d_nodeManager);
 218     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
 219     Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
 220     d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::IFF, a, b), false, false );
 221     TS_ASSERT( d_satSolver->addClauseCalled() );
 222   }
 223
 224   void testImplies() {
 225     NodeManagerScope nms(d_nodeManager);
 226     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
 227     Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
 228     d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::IMPLIES, a, b), false, false );
 229     TS_ASSERT( d_satSolver->addClauseCalled() );
 230   }
 231
 232   // ITEs should be removed before going to CNF
 233   //void testIte() {
 234   //  NodeManagerScope nms(d_nodeManager);
 235   //  d_cnfStream->convertAndAssert(
 236   //      d_nodeManager->mkNode(
 237   //          kind::EQUAL,
 238   //          d_nodeManager->mkNode(
 239   //              kind::ITE,
 240   //              d_nodeManager->mkVar(d_nodeManager->booleanType()),
 241   //              d_nodeManager->mkVar(d_nodeManager->integerType()),
 242   //              d_nodeManager->mkVar(d_nodeManager->integerType())
 243   //          ),
 244   //          d_nodeManager->mkVar(d_nodeManager->integerType())
 245   //                            ), false, false);
 246   //
 247   //}
 248
 249   void testNot() {
 250     NodeManagerScope nms(d_nodeManager);
 251     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
 252     d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::NOT, a), false, false );
 253     TS_ASSERT( d_satSolver->addClauseCalled() );
 254   }
 255
 256   void testOr() {
 257     NodeManagerScope nms(d_nodeManager);
 258     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
 259     Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
 260     Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
 261     d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::OR, a, b, c), false, false );
 262     TS_ASSERT( d_satSolver->addClauseCalled() );
 263   }
 264
 265   void testVar() {
 266     NodeManagerScope nms(d_nodeManager);
 267     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
 268     Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
 269     d_cnfStream->convertAndAssert(a, false, false);
 270     TS_ASSERT( d_satSolver->addClauseCalled() );
 271     d_satSolver->reset();
 272     d_cnfStream->convertAndAssert(b, false, false);
 273     TS_ASSERT( d_satSolver->addClauseCalled() );
 274   }
 275
 276   void testXor() {
 277     NodeManagerScope nms(d_nodeManager);
 278     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
 279     Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
 280     d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::XOR, a, b), false, false );
 281     TS_ASSERT( d_satSolver->addClauseCalled() );
 282   }
 283
 284   void testEnsureLiteral() {
 285     NodeManagerScope nms(d_nodeManager);
 286     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
 287     Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
 288     Node a_and_b = d_nodeManager->mkNode(kind::AND, a, b);
 289     d_cnfStream->ensureLiteral(a_and_b);
 290     // Clauses are necessary to "literal-ize" a_and_b; this perhaps
 291     // doesn't belong in a black-box test though...
 292     TS_ASSERT( d_satSolver->addClauseCalled() );
 293     TS_ASSERT( d_cnfStream->hasLiteral(a_and_b) );
 294   }
 295 };