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_theoryEngine = new TheoryEngine(d_context, d_userContext, *d_logicInfo);
 150     d_theoryEngine->addTheory<theory::builtin::TheoryBuiltin>(theory::THEORY_BUILTIN);
 151     d_theoryEngine->addTheory<theory::booleans::TheoryBool>(theory::THEORY_BOOL);
 152     d_theoryEngine->addTheory<theory::arith::TheoryArith>(theory::THEORY_ARITH);
 153     d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, new theory::TheoryRegistrar(d_theoryEngine));
 154   }
 155
 156   void tearDown() {
 157     NodeManagerScope nms(d_nodeManager);
 158     delete d_cnfStream;
 159     d_theoryEngine->shutdown();
 160     delete d_theoryEngine;
 161     delete d_logicInfo;
 162     delete d_satSolver;
 163     delete d_nodeManager;
 164     delete d_userContext;
 165     delete d_context;
 166   }
 167
 168 public:
 169
 170   /* [chris 5/26/2010] In the tests below, we don't attempt to delve into the
 171    * deep structure of the CNF conversion. Firstly, we just want to make sure
 172    * that the conversion doesn't choke on any boolean Exprs. We'll also check
 173    * that addClause got called. We won't check that it gets called a particular
 174    * number of times, or with what.
 175    */
 176
 177   void testAnd() {
 178     NodeManagerScope nms(d_nodeManager);
 179     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
 180     Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
 181     Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
 182     d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::AND, a, b, c), false, false);
 183     TS_ASSERT( d_satSolver->addClauseCalled() );
 184   }
 185
 186   void testComplexExpr() {
 187     NodeManagerScope nms(d_nodeManager);
 188     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
 189     Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
 190     Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
 191     Node d = d_nodeManager->mkVar(d_nodeManager->booleanType());
 192     Node e = d_nodeManager->mkVar(d_nodeManager->booleanType());
 193     Node f = d_nodeManager->mkVar(d_nodeManager->booleanType());
 194     d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::IMPLIES,
 195                                                         d_nodeManager->mkNode(kind::AND, a, b),
 196                                                         d_nodeManager->mkNode(kind::IFF,
 197                                                                               d_nodeManager->mkNode(kind::OR, c, d),
 198                                                                               d_nodeManager->mkNode(kind::NOT,
 199                                                                                                     d_nodeManager->mkNode(kind::XOR, e, f)))), false, false );
 200     TS_ASSERT( d_satSolver->addClauseCalled() );
 201   }
 202
 203   void testFalse() {
 204     NodeManagerScope nms(d_nodeManager);
 205     d_cnfStream->convertAndAssert(  d_nodeManager->mkConst(false), false, false );
 206     TS_ASSERT( d_satSolver->addClauseCalled() );
 207   }
 208
 209   void testIff() {
 210     NodeManagerScope nms(d_nodeManager);
 211     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
 212     Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
 213     d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::IFF, a, b), false, false );
 214     TS_ASSERT( d_satSolver->addClauseCalled() );
 215   }
 216
 217   void testImplies() {
 218     NodeManagerScope nms(d_nodeManager);
 219     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
 220     Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
 221     d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::IMPLIES, a, b), false, false );
 222     TS_ASSERT( d_satSolver->addClauseCalled() );
 223   }
 224
 225   // ITEs should be removed before going to CNF
 226   //void testIte() {
 227   //  NodeManagerScope nms(d_nodeManager);
 228   //  d_cnfStream->convertAndAssert(
 229   //      d_nodeManager->mkNode(
 230   //          kind::EQUAL,
 231   //          d_nodeManager->mkNode(
 232   //              kind::ITE,
 233   //              d_nodeManager->mkVar(d_nodeManager->booleanType()),
 234   //              d_nodeManager->mkVar(d_nodeManager->integerType()),
 235   //              d_nodeManager->mkVar(d_nodeManager->integerType())
 236   //          ),
 237   //          d_nodeManager->mkVar(d_nodeManager->integerType())
 238   //                            ), false, false);
 239   //
 240   //}
 241
 242   void testNot() {
 243     NodeManagerScope nms(d_nodeManager);
 244     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
 245     d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::NOT, a), false, false );
 246     TS_ASSERT( d_satSolver->addClauseCalled() );
 247   }
 248
 249   void testOr() {
 250     NodeManagerScope nms(d_nodeManager);
 251     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
 252     Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
 253     Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
 254     d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::OR, a, b, c), false, false );
 255     TS_ASSERT( d_satSolver->addClauseCalled() );
 256   }
 257
 258   void testTrue() {
 259     NodeManagerScope nms(d_nodeManager);
 260     d_cnfStream->convertAndAssert(  d_nodeManager->mkConst(true), false, false );
 261     TS_ASSERT( d_satSolver->addClauseCalled() );
 262   }
 263
 264   void testVar() {
 265     NodeManagerScope nms(d_nodeManager);
 266     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
 267     Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
 268     d_cnfStream->convertAndAssert(a, false, false);
 269     TS_ASSERT( d_satSolver->addClauseCalled() );
 270     d_satSolver->reset();
 271     d_cnfStream->convertAndAssert(b, false, false);
 272     TS_ASSERT( d_satSolver->addClauseCalled() );
 273   }
 274
 275   void testXor() {
 276     NodeManagerScope nms(d_nodeManager);
 277     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
 278     Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
 279     d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::XOR, a, b), false, false );
 280     TS_ASSERT( d_satSolver->addClauseCalled() );
 281   }
 282
 283   void testEnsureLiteral() {
 284     NodeManagerScope nms(d_nodeManager);
 285     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
 286     Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
 287     Node a_and_b = d_nodeManager->mkNode(kind::AND, a, b);
 288     d_cnfStream->ensureLiteral(a_and_b);
 289     // Clauses are necessary to "literal-ize" a_and_b; this perhaps
 290     // doesn't belong in a black-box test though...
 291     TS_ASSERT( d_satSolver->addClauseCalled() );
 292     TS_ASSERT( d_cnfStream->hasLiteral(a_and_b) );
 293   }
 294 };