Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	test/unit/prop/cnf_stream_white.cpp	Lines:	106	118	89.8 %
Date:	2021-09-18	Branches:	182	468	38.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->getEnv(),
                                  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)
{
  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)
{
  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)
{
  d_cnfStream->convertAndAssert(d_nodeManager->mkConst(true), false, false);
  ASSERT_TRUE(d_satSolver->addClauseCalled());
}

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

TEST_F(TestPropWhiteCnfStream, iff)
{
  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)
{
  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 )
{
  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)
{
  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)
{
  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)
{
  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)
{
  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->getEnv(),
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	Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
154	4	Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
155	4	Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
156	4	d_cnfStream->convertAndAssert(
157	4	d_nodeManager->mkNode(kind::AND, a, b, c), false, false);
158	2	ASSERT_TRUE(d_satSolver->addClauseCalled());
159		}
160
161	20	TEST_F(TestPropWhiteCnfStream, complex_expr)
162		{
163	4	Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
164	4	Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
165	4	Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
166	4	Node d = d_nodeManager->mkVar(d_nodeManager->booleanType());
167	4	Node e = d_nodeManager->mkVar(d_nodeManager->booleanType());
168	4	Node f = d_nodeManager->mkVar(d_nodeManager->booleanType());
169	4	d_cnfStream->convertAndAssert(
170	10	d_nodeManager->mkNode(
171		kind::IMPLIES,
172	4	d_nodeManager->mkNode(kind::AND, a, b),
173	10	d_nodeManager->mkNode(
174		kind::EQUAL,
175	4	d_nodeManager->mkNode(kind::OR, c, d),
176	6	d_nodeManager->mkNode(kind::NOT,
177	4	d_nodeManager->mkNode(kind::XOR, e, f)))),
178		false,
179		false);
180	2	ASSERT_TRUE(d_satSolver->addClauseCalled());
181		}
182
183	20	TEST_F(TestPropWhiteCnfStream, true)
184		{
185	2	d_cnfStream->convertAndAssert(d_nodeManager->mkConst(true), false, false);
186	2	ASSERT_TRUE(d_satSolver->addClauseCalled());
187		}
188
189	20	TEST_F(TestPropWhiteCnfStream, false)
190		{
191	2	d_cnfStream->convertAndAssert(d_nodeManager->mkConst(false), false, false);
192	2	ASSERT_TRUE(d_satSolver->addClauseCalled());
193		}
194
195	20	TEST_F(TestPropWhiteCnfStream, iff)
196		{
197	4	Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
198	4	Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
199	4	d_cnfStream->convertAndAssert(
200	4	d_nodeManager->mkNode(kind::EQUAL, a, b), false, false);
201	2	ASSERT_TRUE(d_satSolver->addClauseCalled());
202		}
203
204	20	TEST_F(TestPropWhiteCnfStream, implies)
205		{
206	4	Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
207	4	Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
208	4	d_cnfStream->convertAndAssert(
209	4	d_nodeManager->mkNode(kind::IMPLIES, a, b), false, false);
210	2	ASSERT_TRUE(d_satSolver->addClauseCalled());
211		}
212
213	20	TEST_F(TestPropWhiteCnfStream, not )
214		{
215	4	Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
216	4	d_cnfStream->convertAndAssert(
217	4	d_nodeManager->mkNode(kind::NOT, a), false, false);
218	2	ASSERT_TRUE(d_satSolver->addClauseCalled());
219		}
220
221	20	TEST_F(TestPropWhiteCnfStream, or)
222		{
223	4	Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
224	4	Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
225	4	Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
226	4	d_cnfStream->convertAndAssert(
227	4	d_nodeManager->mkNode(kind::OR, a, b, c), false, false);
228	2	ASSERT_TRUE(d_satSolver->addClauseCalled());
229		}
230
231	20	TEST_F(TestPropWhiteCnfStream, var)
232		{
233	4	Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
234	4	Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
235	2	d_cnfStream->convertAndAssert(a, false, false);
236	2	ASSERT_TRUE(d_satSolver->addClauseCalled());
237	2	d_satSolver->reset();
238	2	d_cnfStream->convertAndAssert(b, false, false);
239	2	ASSERT_TRUE(d_satSolver->addClauseCalled());
240		}
241
242	20	TEST_F(TestPropWhiteCnfStream, xor)
243		{
244	4	Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
245	4	Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
246	4	d_cnfStream->convertAndAssert(
247	4	d_nodeManager->mkNode(kind::XOR, a, b), false, false);
248	2	ASSERT_TRUE(d_satSolver->addClauseCalled());
249		}
250
251	20	TEST_F(TestPropWhiteCnfStream, ensure_literal)
252		{
253	4	Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
254	4	Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
255	4	Node a_and_b = d_nodeManager->mkNode(kind::AND, a, b);
256	2	d_cnfStream->ensureLiteral(a_and_b);
257		// Clauses are necessary to "literal-ize" a_and_b
258	2	ASSERT_TRUE(d_satSolver->addClauseCalled());
259	2	ASSERT_TRUE(d_cnfStream->hasLiteral(a_and_b));
260		}
261		} // namespace test
262	36	} // namespace cvc5