Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	test/unit/prop/cnf_stream_white.cpp	Lines:	117	129	90.7 %
Date:	2021-05-22	Branches:	205	514	39.9 %


/******************************************************************************
 * Top contributors (to current version):
 *   Aina Niemetz, Christopher L. Conway, Andres Noetzli
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * White box testing of cvc5::prop::CnfStream.
 */

#include "base/check.h"
#include "context/context.h"
#include "prop/cnf_stream.h"
#include "prop/prop_engine.h"
#include "prop/registrar.h"
#include "prop/sat_solver.h"
#include "prop/theory_proxy.h"
#include "test_smt.h"
#include "theory/arith/theory_arith.h"
#include "theory/booleans/theory_bool.h"
#include "theory/builtin/theory_builtin.h"
#include "theory/theory.h"
#include "theory/theory_engine.h"

namespace cvc5 {

using namespace context;
using namespace prop;
using namespace smt;
using namespace theory;

namespace test {

/* This fake class relies on the fact that a MiniSat variable is just an int. */
class FakeSatSolver : public SatSolver
{
 public:
  FakeSatSolver() : d_nextVar(0), d_addClauseCalled(false) {}

  SatVariable newVar(bool theoryAtom, bool preRegister, bool canErase) override
  {
    return d_nextVar++;
  }

  SatVariable trueVar() override { return d_nextVar++; }

  SatVariable falseVar() override { return d_nextVar++; }

  ClauseId addClause(SatClause& c, bool lemma) override
  {
    d_addClauseCalled = true;
    return ClauseIdUndef;
  }

  ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override
  {
    d_addClauseCalled = true;
    return ClauseIdUndef;
  }

  bool nativeXor() override { return false; }

  void reset() { d_addClauseCalled = false; }

  unsigned int addClauseCalled() { return d_addClauseCalled; }

  unsigned getAssertionLevel() const override { return 0; }

  bool isDecision(Node) const { return false; }

  void unregisterVar(SatLiteral lit) {}

  void renewVar(SatLiteral lit, int level = -1) {}

  bool spendResource() { return false; }

  void interrupt() override {}

  SatValue solve() override { return SAT_VALUE_UNKNOWN; }

  SatValue solve(long unsigned int& resource) override
  {
    return SAT_VALUE_UNKNOWN;
  }

  SatValue value(SatLiteral l) override { return SAT_VALUE_UNKNOWN; }

  SatValue modelValue(SatLiteral l) override { return SAT_VALUE_UNKNOWN; }

  bool properExplanation(SatLiteral lit, SatLiteral expl) const { return true; }

  bool ok() const override { return true; }

 private:
  SatVariable d_nextVar;
  bool d_addClauseCalled;
};

class TestPropWhiteCnfStream : public TestSmt
{
 protected:
  void SetUp() override
  {
    TestSmt::SetUp();
    d_theoryEngine = d_smtEngine->getTheoryEngine();
    d_satSolver.reset(new FakeSatSolver());
    d_cnfContext.reset(new context::Context());
    d_cnfRegistrar.reset(new prop::NullRegistrar);
    d_cnfStream.reset(
        new cvc5::prop::CnfStream(d_satSolver.get(),
                                  d_cnfRegistrar.get(),
                                  d_cnfContext.get(),
                                  &d_smtEngine->getOutputManager(),
                                  d_smtEngine->getResourceManager()));
  }

  void TearDown() override
  {
    d_cnfStream.reset(nullptr);
    d_cnfRegistrar.reset(nullptr);
    d_cnfContext.reset(nullptr);
    d_satSolver.reset(nullptr);
    TestSmt::TearDown();
  }

  /** The SAT solver proxy */
  std::unique_ptr<FakeSatSolver> d_satSolver;
  /** The theory engine */
  TheoryEngine* d_theoryEngine;
  /** The CNF converter in use */
  std::unique_ptr<CnfStream> d_cnfStream;
  /** The context of the CnfStream. */
  std::unique_ptr<Context> d_cnfContext;
  /** The registrar used by the CnfStream. */
  std::unique_ptr<prop::NullRegistrar> d_cnfRegistrar;
};

/**
 * [chris 5/26/2010] In the tests below, we don't attempt to delve into the
 * deep structure of the CNF conversion. Firstly, we just want to make sure
 * that the conversion doesn't choke on any boolean Exprs. We'll also check
 * that addClause got called. We won't check that it gets called a particular
 * number of times, or with what.
 */

TEST_F(TestPropWhiteCnfStream, and)
{
  NodeManagerScope nms(d_nodeManager.get());
  Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
  Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
  Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
  d_cnfStream->convertAndAssert(
      d_nodeManager->mkNode(kind::AND, a, b, c), false, false);
  ASSERT_TRUE(d_satSolver->addClauseCalled());
}

TEST_F(TestPropWhiteCnfStream, complex_expr)
{
  NodeManagerScope nms(d_nodeManager.get());
  Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
  Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
  Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
  Node d = d_nodeManager->mkVar(d_nodeManager->booleanType());
  Node e = d_nodeManager->mkVar(d_nodeManager->booleanType());
  Node f = d_nodeManager->mkVar(d_nodeManager->booleanType());
  d_cnfStream->convertAndAssert(
      d_nodeManager->mkNode(
          kind::IMPLIES,
          d_nodeManager->mkNode(kind::AND, a, b),
          d_nodeManager->mkNode(
              kind::EQUAL,
              d_nodeManager->mkNode(kind::OR, c, d),
              d_nodeManager->mkNode(kind::NOT,
                                    d_nodeManager->mkNode(kind::XOR, e, f)))),
      false,
      false);
  ASSERT_TRUE(d_satSolver->addClauseCalled());
}

TEST_F(TestPropWhiteCnfStream, true)
{
  NodeManagerScope nms(d_nodeManager.get());
  d_cnfStream->convertAndAssert(d_nodeManager->mkConst(true), false, false);
  ASSERT_TRUE(d_satSolver->addClauseCalled());
}

TEST_F(TestPropWhiteCnfStream, false)
{
  NodeManagerScope nms(d_nodeManager.get());
  d_cnfStream->convertAndAssert(d_nodeManager->mkConst(false), false, false);
  ASSERT_TRUE(d_satSolver->addClauseCalled());
}

TEST_F(TestPropWhiteCnfStream, iff)
{
  NodeManagerScope nms(d_nodeManager.get());
  Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
  Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
  d_cnfStream->convertAndAssert(
      d_nodeManager->mkNode(kind::EQUAL, a, b), false, false);
  ASSERT_TRUE(d_satSolver->addClauseCalled());
}

TEST_F(TestPropWhiteCnfStream, implies)
{
  NodeManagerScope nms(d_nodeManager.get());
  Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
  Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
  d_cnfStream->convertAndAssert(
      d_nodeManager->mkNode(kind::IMPLIES, a, b), false, false);
  ASSERT_TRUE(d_satSolver->addClauseCalled());
}

TEST_F(TestPropWhiteCnfStream, not )
{
  NodeManagerScope nms(d_nodeManager.get());
  Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
  d_cnfStream->convertAndAssert(
      d_nodeManager->mkNode(kind::NOT, a), false, false);
  ASSERT_TRUE(d_satSolver->addClauseCalled());
}

TEST_F(TestPropWhiteCnfStream, or)
{
  NodeManagerScope nms(d_nodeManager.get());
  Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
  Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
  Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
  d_cnfStream->convertAndAssert(
      d_nodeManager->mkNode(kind::OR, a, b, c), false, false);
  ASSERT_TRUE(d_satSolver->addClauseCalled());
}

TEST_F(TestPropWhiteCnfStream, var)
{
  NodeManagerScope nms(d_nodeManager.get());
  Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
  Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
  d_cnfStream->convertAndAssert(a, false, false);
  ASSERT_TRUE(d_satSolver->addClauseCalled());
  d_satSolver->reset();
  d_cnfStream->convertAndAssert(b, false, false);
  ASSERT_TRUE(d_satSolver->addClauseCalled());
}

TEST_F(TestPropWhiteCnfStream, xor)
{
  NodeManagerScope nms(d_nodeManager.get());
  Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
  Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
  d_cnfStream->convertAndAssert(
      d_nodeManager->mkNode(kind::XOR, a, b), false, false);
  ASSERT_TRUE(d_satSolver->addClauseCalled());
}

TEST_F(TestPropWhiteCnfStream, ensure_literal)
{
  NodeManagerScope nms(d_nodeManager.get());
  Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
  Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
  Node a_and_b = d_nodeManager->mkNode(kind::AND, a, b);
  d_cnfStream->ensureLiteral(a_and_b);
  // Clauses are necessary to "literal-ize" a_and_b
  ASSERT_TRUE(d_satSolver->addClauseCalled());
  ASSERT_TRUE(d_cnfStream->hasLiteral(a_and_b));
}
}  // namespace test
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Aina Niemetz, Christopher L. Conway, Andres Noetzli
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* White box testing of cvc5::prop::CnfStream.
14		*/
15
16		#include "base/check.h"
17		#include "context/context.h"
18		#include "prop/cnf_stream.h"
19		#include "prop/prop_engine.h"
20		#include "prop/registrar.h"
21		#include "prop/sat_solver.h"
22		#include "prop/theory_proxy.h"
23		#include "test_smt.h"
24		#include "theory/arith/theory_arith.h"
25		#include "theory/booleans/theory_bool.h"
26		#include "theory/builtin/theory_builtin.h"
27		#include "theory/theory.h"
28		#include "theory/theory_engine.h"
29
30		namespace cvc5 {
31
32		using namespace context;
33		using namespace prop;
34		using namespace smt;
35		using namespace theory;
36
37		namespace test {
38
39		/* This fake class relies on the fact that a MiniSat variable is just an int. */
40	44	class FakeSatSolver : public SatSolver
41		{
42		public:
43	22	FakeSatSolver() : d_nextVar(0), d_addClauseCalled(false) {}
44
45	56	SatVariable newVar(bool theoryAtom, bool preRegister, bool canErase) override
46		{
47	56	return d_nextVar++;
48		}
49
50	2	SatVariable trueVar() override { return d_nextVar++; }
51
52	2	SatVariable falseVar() override { return d_nextVar++; }
53
54	64	ClauseId addClause(SatClause& c, bool lemma) override
55		{
56	64	d_addClauseCalled = true;
57	64	return ClauseIdUndef;
58		}
59
60		ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override
61		{
62		d_addClauseCalled = true;
63		return ClauseIdUndef;
64		}
65
66		bool nativeXor() override { return false; }
67
68	2	void reset() { d_addClauseCalled = false; }
69
70	24	unsigned int addClauseCalled() { return d_addClauseCalled; }
71
72		unsigned getAssertionLevel() const override { return 0; }
73
74		bool isDecision(Node) const { return false; }
75
76		void unregisterVar(SatLiteral lit) {}
77
78		void renewVar(SatLiteral lit, int level = -1) {}
79
80		bool spendResource() { return false; }
81
82		void interrupt() override {}
83
84		SatValue solve() override { return SAT_VALUE_UNKNOWN; }
85
86		SatValue solve(long unsigned int& resource) override
87		{
88		return SAT_VALUE_UNKNOWN;
89		}
90
91		SatValue value(SatLiteral l) override { return SAT_VALUE_UNKNOWN; }
92
93		SatValue modelValue(SatLiteral l) override { return SAT_VALUE_UNKNOWN; }
94
95		bool properExplanation(SatLiteral lit, SatLiteral expl) const { return true; }
96
97		bool ok() const override { return true; }
98
99		private:
100		SatVariable d_nextVar;
101		bool d_addClauseCalled;
102		};
103
104	44	class TestPropWhiteCnfStream : public TestSmt
105		{
106		protected:
107	22	void SetUp() override
108		{
109	22	TestSmt::SetUp();
110	22	d_theoryEngine = d_smtEngine->getTheoryEngine();
111	22	d_satSolver.reset(new FakeSatSolver());
112	22	d_cnfContext.reset(new context::Context());
113	22	d_cnfRegistrar.reset(new prop::NullRegistrar);
114	66	d_cnfStream.reset(
115	22	new cvc5::prop::CnfStream(d_satSolver.get(),
116	22	d_cnfRegistrar.get(),
117	22	d_cnfContext.get(),
118	22	&d_smtEngine->getOutputManager(),
119	44	d_smtEngine->getResourceManager()));
120	22	}
121
122	22	void TearDown() override
123		{
124	22	d_cnfStream.reset(nullptr);
125	22	d_cnfRegistrar.reset(nullptr);
126	22	d_cnfContext.reset(nullptr);
127	22	d_satSolver.reset(nullptr);
128	22	TestSmt::TearDown();
129	22	}
130
131		/** The SAT solver proxy */
132		std::unique_ptr<FakeSatSolver> d_satSolver;
133		/** The theory engine */
134		TheoryEngine* d_theoryEngine;
135		/** The CNF converter in use */
136		std::unique_ptr<CnfStream> d_cnfStream;
137		/** The context of the CnfStream. */
138		std::unique_ptr<Context> d_cnfContext;
139		/** The registrar used by the CnfStream. */
140		std::unique_ptr<prop::NullRegistrar> d_cnfRegistrar;
141		};
142
143		/**
144		* [chris 5/26/2010] In the tests below, we don't attempt to delve into the
145		* deep structure of the CNF conversion. Firstly, we just want to make sure
146		* that the conversion doesn't choke on any boolean Exprs. We'll also check
147		* that addClause got called. We won't check that it gets called a particular
148		* number of times, or with what.
149		*/
150
151	20	TEST_F(TestPropWhiteCnfStream, and)
152		{
153	4	NodeManagerScope nms(d_nodeManager.get());
154	4	Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
155	4	Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
156	4	Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
157	4	d_cnfStream->convertAndAssert(
158	4	d_nodeManager->mkNode(kind::AND, a, b, c), false, false);
159	2	ASSERT_TRUE(d_satSolver->addClauseCalled());
160		}
161
162	20	TEST_F(TestPropWhiteCnfStream, complex_expr)
163		{
164	4	NodeManagerScope nms(d_nodeManager.get());
165	4	Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
166	4	Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
167	4	Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
168	4	Node d = d_nodeManager->mkVar(d_nodeManager->booleanType());
169	4	Node e = d_nodeManager->mkVar(d_nodeManager->booleanType());
170	4	Node f = d_nodeManager->mkVar(d_nodeManager->booleanType());
171	4	d_cnfStream->convertAndAssert(
172	10	d_nodeManager->mkNode(
173		kind::IMPLIES,
174	4	d_nodeManager->mkNode(kind::AND, a, b),
175	10	d_nodeManager->mkNode(
176		kind::EQUAL,
177	4	d_nodeManager->mkNode(kind::OR, c, d),
178	6	d_nodeManager->mkNode(kind::NOT,
179	4	d_nodeManager->mkNode(kind::XOR, e, f)))),
180		false,
181		false);
182	2	ASSERT_TRUE(d_satSolver->addClauseCalled());
183		}
184
185	20	TEST_F(TestPropWhiteCnfStream, true)
186		{
187	4	NodeManagerScope nms(d_nodeManager.get());
188	2	d_cnfStream->convertAndAssert(d_nodeManager->mkConst(true), false, false);
189	2	ASSERT_TRUE(d_satSolver->addClauseCalled());
190		}
191
192	20	TEST_F(TestPropWhiteCnfStream, false)
193		{
194	4	NodeManagerScope nms(d_nodeManager.get());
195	2	d_cnfStream->convertAndAssert(d_nodeManager->mkConst(false), false, false);
196	2	ASSERT_TRUE(d_satSolver->addClauseCalled());
197		}
198
199	20	TEST_F(TestPropWhiteCnfStream, iff)
200		{
201	4	NodeManagerScope nms(d_nodeManager.get());
202	4	Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
203	4	Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
204	4	d_cnfStream->convertAndAssert(
205	4	d_nodeManager->mkNode(kind::EQUAL, a, b), false, false);
206	2	ASSERT_TRUE(d_satSolver->addClauseCalled());
207		}
208
209	20	TEST_F(TestPropWhiteCnfStream, implies)
210		{
211	4	NodeManagerScope nms(d_nodeManager.get());
212	4	Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
213	4	Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
214	4	d_cnfStream->convertAndAssert(
215	4	d_nodeManager->mkNode(kind::IMPLIES, a, b), false, false);
216	2	ASSERT_TRUE(d_satSolver->addClauseCalled());
217		}
218
219	20	TEST_F(TestPropWhiteCnfStream, not )
220		{
221	4	NodeManagerScope nms(d_nodeManager.get());
222	4	Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
223	4	d_cnfStream->convertAndAssert(
224	4	d_nodeManager->mkNode(kind::NOT, a), false, false);
225	2	ASSERT_TRUE(d_satSolver->addClauseCalled());
226		}
227
228	20	TEST_F(TestPropWhiteCnfStream, or)
229		{
230	4	NodeManagerScope nms(d_nodeManager.get());
231	4	Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
232	4	Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
233	4	Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
234	4	d_cnfStream->convertAndAssert(
235	4	d_nodeManager->mkNode(kind::OR, a, b, c), false, false);
236	2	ASSERT_TRUE(d_satSolver->addClauseCalled());
237		}
238
239	20	TEST_F(TestPropWhiteCnfStream, var)
240		{
241	4	NodeManagerScope nms(d_nodeManager.get());
242	4	Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
243	4	Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
244	2	d_cnfStream->convertAndAssert(a, false, false);
245	2	ASSERT_TRUE(d_satSolver->addClauseCalled());
246	2	d_satSolver->reset();
247	2	d_cnfStream->convertAndAssert(b, false, false);
248	2	ASSERT_TRUE(d_satSolver->addClauseCalled());
249		}
250
251	20	TEST_F(TestPropWhiteCnfStream, xor)
252		{
253	4	NodeManagerScope nms(d_nodeManager.get());
254	4	Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
255	4	Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
256	4	d_cnfStream->convertAndAssert(
257	4	d_nodeManager->mkNode(kind::XOR, a, b), false, false);
258	2	ASSERT_TRUE(d_satSolver->addClauseCalled());
259		}
260
261	20	TEST_F(TestPropWhiteCnfStream, ensure_literal)
262		{
263	4	NodeManagerScope nms(d_nodeManager.get());
264	4	Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
265	4	Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
266	4	Node a_and_b = d_nodeManager->mkNode(kind::AND, a, b);
267	2	d_cnfStream->ensureLiteral(a_and_b);
268		// Clauses are necessary to "literal-ize" a_and_b
269	2	ASSERT_TRUE(d_satSolver->addClauseCalled());
270	2	ASSERT_TRUE(d_cnfStream->hasLiteral(a_and_b));
271		}
272		} // namespace test
273	150800	} // namespace cvc5