Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	test/unit/test_smt.h	Lines:	39	68	57.4 %
Date:	2021-09-29	Branches:	25	141	17.7 %


/******************************************************************************
 * Top contributors (to current version):
 *   Aina Niemetz, Andrew Reynolds, Haniel Barbosa
 *
 * 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.
 * ****************************************************************************
 *
 * Common header for unit tests that need an SmtEngine.
 */

#ifndef CVC5__TEST__UNIT__TEST_SMT_H
#define CVC5__TEST__UNIT__TEST_SMT_H

#include "expr/dtype_cons.h"
#include "expr/node.h"
#include "expr/node_manager.h"
#include "expr/skolem_manager.h"
#include "proof/proof_checker.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
#include "test.h"
#include "theory/output_channel.h"
#include "theory/rewriter.h"
#include "theory/theory.h"
#include "theory/theory_state.h"
#include "theory/valuation.h"
#include "util/resource_manager.h"
#include "util/unsafe_interrupt_exception.h"

namespace cvc5 {
namespace test {

/* -------------------------------------------------------------------------- */
/* Test fixtures.                                                             */
/* -------------------------------------------------------------------------- */

class TestSmt : public TestInternal
{
 protected:
  void SetUp() override
  {
    d_nodeManager = NodeManager::currentNM();
    d_nodeManager->init();
    d_skolemManager = d_nodeManager->getSkolemManager();
    d_smtEngine.reset(new SmtEngine(d_nodeManager));
    d_smtEngine->finishInit();
  }

  NodeManager* d_nodeManager;
  SkolemManager* d_skolemManager;
  std::unique_ptr<SmtEngine> d_smtEngine;
};

class TestSmtNoFinishInit : public TestInternal
{
 protected:
  void SetUp() override
  {
    d_nodeManager = NodeManager::currentNM();
    d_nodeManager->init();
    d_skolemManager = d_nodeManager->getSkolemManager();
    d_smtEngine.reset(new SmtEngine(d_nodeManager));
  }

  NodeManager* d_nodeManager;
  SkolemManager* d_skolemManager;
  std::unique_ptr<SmtEngine> d_smtEngine;
};

/* -------------------------------------------------------------------------- */
/* Helpers.                                                                   */
/* -------------------------------------------------------------------------- */

/**
 * Very basic OutputChannel for testing simple Theory Behaviour.
 * Stores a call sequence for the output channel
 */
enum OutputChannelCallType
{
  CONFLICT,
  PROPAGATE,
  PROPAGATE_AS_DECISION,
  AUG_LEMMA,
  LEMMA,
  EXPLANATION
};

inline std::ostream& operator<<(std::ostream& out, OutputChannelCallType type)
{
  switch (type)
  {
    case CONFLICT: return out << "CONFLICT";
    case PROPAGATE: return out << "PROPAGATE";
    case PROPAGATE_AS_DECISION: return out << "PROPAGATE_AS_DECISION";
    case AUG_LEMMA: return out << "AUG_LEMMA";
    case LEMMA: return out << "LEMMA";
    case EXPLANATION: return out << "EXPLANATION";
    default: return out << "UNDEFINED-OutputChannelCallType!" << int(type);
  }
}

class DummyOutputChannel : public cvc5::theory::OutputChannel
{
 public:
  DummyOutputChannel() {}
  ~DummyOutputChannel() override {}

  void safePoint(Resource r) override {}
  void conflict(TNode n) override { push(CONFLICT, n); }

  void trustedConflict(TrustNode n) override { push(CONFLICT, n.getNode()); }

  bool propagate(TNode n) override
  {
    push(PROPAGATE, n);
    return true;
  }

  void lemma(TNode n,
             theory::LemmaProperty p = theory::LemmaProperty::NONE) override
  {
    push(LEMMA, n);
  }

  void trustedLemma(TrustNode n, theory::LemmaProperty p) override
  {
    push(LEMMA, n.getNode());
  }

  void requirePhase(TNode, bool) override {}
  void setIncomplete(theory::IncompleteId id) override {}

  void clear() { d_callHistory.clear(); }

  Node getIthNode(int i) const
  {
    Node tmp = (d_callHistory[i]).second;
    return tmp;
  }

  OutputChannelCallType getIthCallType(int i) const
  {
    return (d_callHistory[i]).first;
  }

  unsigned getNumCalls() const { return d_callHistory.size(); }

  void printIth(std::ostream& os, int i) const
  {
    os << "[DummyOutputChannel " << i;
    os << " " << getIthCallType(i);
    os << " " << getIthNode(i) << "]";
  }

 private:
  void push(OutputChannelCallType call, TNode n)
  {
    d_callHistory.push_back(std::make_pair(call, n));
  }

  std::vector<std::pair<enum OutputChannelCallType, Node> > d_callHistory;
};

/* -------------------------------------------------------------------------- */

class DummyTheoryRewriter : public theory::TheoryRewriter
{
 public:
  theory::RewriteResponse preRewrite(TNode n) override
  {
    return theory::RewriteResponse(theory::REWRITE_DONE, n);
  }

  theory::RewriteResponse postRewrite(TNode n) override
  {
    return theory::RewriteResponse(theory::REWRITE_DONE, n);
  }
};

class DummyProofRuleChecker : public ProofRuleChecker
{
 public:
  DummyProofRuleChecker() {}
  ~DummyProofRuleChecker() {}
  void registerTo(ProofChecker* pc) override {}

 protected:
  Node checkInternal(PfRule id,
                     const std::vector<Node>& children,
                     const std::vector<Node>& args) override
  {
    return Node::null();
  }
};

/** Dummy Theory interface.  */
template <theory::TheoryId theoryId>
class DummyTheory : public theory::Theory
{
 public:
  DummyTheory(Env& env, theory::OutputChannel& out, theory::Valuation valuation)
      : Theory(theoryId, env, out, valuation),
        d_state(env, valuation)
  {
    // use a default theory state object
    d_theoryState = &d_state;
  }

  theory::TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
  ProofRuleChecker* getProofChecker() override { return &d_checker; }

  void registerTerm(TNode n)
  {
    // check that we registerTerm() a term only once
    ASSERT_TRUE(d_registered.find(n) == d_registered.end());

    for (TNode::iterator i = n.begin(); i != n.end(); ++i)
    {
      // check that registerTerm() is called in reverse topological order
      ASSERT_TRUE(d_registered.find(*i) != d_registered.end());
    }

    d_registered.insert(n);
  }

  void presolve() override { Unimplemented(); }
  void preRegisterTerm(TNode n) override { Unimplemented(); }
  void propagate(Effort level) override { Unimplemented(); }
  bool preNotifyFact(
      TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal) override
  {
    // do not assert to equality engine, since this theory does not use one
    return true;
  }
  TrustNode explain(TNode n) override { return TrustNode::null(); }
  Node getValue(TNode n) { return Node::null(); }
  std::string identify() const override { return "DummyTheory" + d_id; }

  std::set<Node> d_registered;

 private:
  /** Default theory state object */
  theory::TheoryState d_state;
  /**
   * This fake theory class is equally useful for bool, uf, arith, etc.  It
   * keeps an identifier to identify itself.
   */
  std::string d_id;
  /** The theory rewriter for this theory. */
  DummyTheoryRewriter d_rewriter;
  /** The proof checker for this theory. */
  DummyProofRuleChecker d_checker;
};

/* -------------------------------------------------------------------------- */
}  // namespace test
}  // namespace cvc5
#endif


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Aina Niemetz, Andrew Reynolds, Haniel Barbosa
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		* Common header for unit tests that need an SmtEngine.
14		*/
15
16		#ifndef CVC5__TEST__UNIT__TEST_SMT_H
17		#define CVC5__TEST__UNIT__TEST_SMT_H
18
19		#include "expr/dtype_cons.h"
20		#include "expr/node.h"
21		#include "expr/node_manager.h"
22		#include "expr/skolem_manager.h"
23		#include "proof/proof_checker.h"
24		#include "smt/smt_engine.h"
25		#include "smt/smt_engine_scope.h"
26		#include "test.h"
27		#include "theory/output_channel.h"
28		#include "theory/rewriter.h"
29		#include "theory/theory.h"
30		#include "theory/theory_state.h"
31		#include "theory/valuation.h"
32		#include "util/resource_manager.h"
33		#include "util/unsafe_interrupt_exception.h"
34
35		namespace cvc5 {
36		namespace test {
37
38		/* -------------------------------------------------------------------------- */
39		/* Test fixtures. */
40		/* -------------------------------------------------------------------------- */
41
42	648	class TestSmt : public TestInternal
43		{
44		protected:
45	324	void SetUp() override
46		{
47	324	d_nodeManager = NodeManager::currentNM();
48	324	d_nodeManager->init();
49	324	d_skolemManager = d_nodeManager->getSkolemManager();
50	324	d_smtEngine.reset(new SmtEngine(d_nodeManager));
51	324	d_smtEngine->finishInit();
52	324	}
53
54		NodeManager* d_nodeManager;
55		SkolemManager* d_skolemManager;
56		std::unique_ptr<SmtEngine> d_smtEngine;
57		};
58
59	1120	class TestSmtNoFinishInit : public TestInternal
60		{
61		protected:
62	560	void SetUp() override
63		{
64	560	d_nodeManager = NodeManager::currentNM();
65	560	d_nodeManager->init();
66	560	d_skolemManager = d_nodeManager->getSkolemManager();
67	560	d_smtEngine.reset(new SmtEngine(d_nodeManager));
68	560	}
69
70		NodeManager* d_nodeManager;
71		SkolemManager* d_skolemManager;
72		std::unique_ptr<SmtEngine> d_smtEngine;
73		};
74
75		/* -------------------------------------------------------------------------- */
76		/* Helpers. */
77		/* -------------------------------------------------------------------------- */
78
79		/**
80		* Very basic OutputChannel for testing simple Theory Behaviour.
81		* Stores a call sequence for the output channel
82		*/
83		enum OutputChannelCallType
84		{
85		CONFLICT,
86		PROPAGATE,
87		PROPAGATE_AS_DECISION,
88		AUG_LEMMA,
89		LEMMA,
90		EXPLANATION
91		};
92
93		inline std::ostream& operator<<(std::ostream& out, OutputChannelCallType type)
94		{
95		switch (type)
96		{
97		case CONFLICT: return out << "CONFLICT";
98		case PROPAGATE: return out << "PROPAGATE";
99		case PROPAGATE_AS_DECISION: return out << "PROPAGATE_AS_DECISION";
100		case AUG_LEMMA: return out << "AUG_LEMMA";
101		case LEMMA: return out << "LEMMA";
102		case EXPLANATION: return out << "EXPLANATION";
103		default: return out << "UNDEFINED-OutputChannelCallType!" << int(type);
104		}
105		}
106
107		class DummyOutputChannel : public cvc5::theory::OutputChannel
108		{
109		public:
110	6	DummyOutputChannel() {}
111	6	~DummyOutputChannel() override {}
112
113		void safePoint(Resource r) override {}
114		void conflict(TNode n) override { push(CONFLICT, n); }
115
116		void trustedConflict(TrustNode n) override { push(CONFLICT, n.getNode()); }
117
118		bool propagate(TNode n) override
119		{
120		push(PROPAGATE, n);
121		return true;
122		}
123
124	4	void lemma(TNode n,
125		theory::LemmaProperty p = theory::LemmaProperty::NONE) override
126		{
127	4	push(LEMMA, n);
128	4	}
129
130		void trustedLemma(TrustNode n, theory::LemmaProperty p) override
131		{
132		push(LEMMA, n.getNode());
133		}
134
135		void requirePhase(TNode, bool) override {}
136		void setIncomplete(theory::IncompleteId id) override {}
137
138	6	void clear() { d_callHistory.clear(); }
139
140		Node getIthNode(int i) const
141		{
142		Node tmp = (d_callHistory[i]).second;
143		return tmp;
144		}
145
146		OutputChannelCallType getIthCallType(int i) const
147		{
148		return (d_callHistory[i]).first;
149		}
150
151		unsigned getNumCalls() const { return d_callHistory.size(); }
152
153		void printIth(std::ostream& os, int i) const
154		{
155		os << "[DummyOutputChannel " << i;
156		os << " " << getIthCallType(i);
157		os << " " << getIthNode(i) << "]";
158		}
159
160		private:
161	4	void push(OutputChannelCallType call, TNode n)
162		{
163	4	d_callHistory.push_back(std::make_pair(call, n));
164	4	}
165
166		std::vector<std::pair<enum OutputChannelCallType, Node> > d_callHistory;
167		};
168
169		/* -------------------------------------------------------------------------- */
170
171	84	class DummyTheoryRewriter : public theory::TheoryRewriter
172		{
173		public:
174	48	theory::RewriteResponse preRewrite(TNode n) override
175		{
176	48	return theory::RewriteResponse(theory::REWRITE_DONE, n);
177		}
178
179	96	theory::RewriteResponse postRewrite(TNode n) override
180		{
181	96	return theory::RewriteResponse(theory::REWRITE_DONE, n);
182		}
183		};
184
185		class DummyProofRuleChecker : public ProofRuleChecker
186		{
187		public:
188	42	DummyProofRuleChecker() {}
189	42	~DummyProofRuleChecker() {}
190		void registerTo(ProofChecker* pc) override {}
191
192		protected:
193		Node checkInternal(PfRule id,
194		const std::vector<Node>& children,
195		const std::vector<Node>& args) override
196		{
197		return Node::null();
198		}
199		};
200
201		/** Dummy Theory interface. */
202		template <theory::TheoryId theoryId>
203	84	class DummyTheory : public theory::Theory
204		{
205		public:
206	42	DummyTheory(Env& env, theory::OutputChannel& out, theory::Valuation valuation)
207		: Theory(theoryId, env, out, valuation),
208	42	d_state(env, valuation)
209		{
210		// use a default theory state object
211	42	d_theoryState = &d_state;
212	42	}
213
214	36	theory::TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
215		ProofRuleChecker* getProofChecker() override { return &d_checker; }
216
217		void registerTerm(TNode n)
218		{
219		// check that we registerTerm() a term only once
220		ASSERT_TRUE(d_registered.find(n) == d_registered.end());
221
222		for (TNode::iterator i = n.begin(); i != n.end(); ++i)
223		{
224		// check that registerTerm() is called in reverse topological order
225		ASSERT_TRUE(d_registered.find(*i) != d_registered.end());
226		}
227
228		d_registered.insert(n);
229		}
230
231		void presolve() override { Unimplemented(); }
232		void preRegisterTerm(TNode n) override { Unimplemented(); }
233		void propagate(Effort level) override { Unimplemented(); }
234	4	bool preNotifyFact(
235		TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal) override
236		{
237		// do not assert to equality engine, since this theory does not use one
238	4	return true;
239		}
240		TrustNode explain(TNode n) override { return TrustNode::null(); }
241		Node getValue(TNode n) { return Node::null(); }
242		std::string identify() const override { return "DummyTheory" + d_id; }
243
244		std::set<Node> d_registered;
245
246		private:
247		/** Default theory state object */
248		theory::TheoryState d_state;
249		/**
250		* This fake theory class is equally useful for bool, uf, arith, etc. It
251		* keeps an identifier to identify itself.
252		*/
253		std::string d_id;
254		/** The theory rewriter for this theory. */
255		DummyTheoryRewriter d_rewriter;
256		/** The proof checker for this theory. */
257		DummyProofRuleChecker d_checker;
258		};
259
260		/* -------------------------------------------------------------------------- */
261		} // namespace test
262		} // namespace cvc5
263		#endif