Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/prop/sat_solver_types.h	Lines:	29	33	87.9 %
Date:	2021-09-10	Branches:	5	16	31.3 %


/******************************************************************************
 * Top contributors (to current version):
 *   Dejan Jovanovic, Alex Ozdemir, Liana Hadarean
 *
 * 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.
 * ****************************************************************************
 *
 * This class transforms a sequence of formulas into clauses.
 *
 * This class takes a sequence of formulas.
 * It outputs a stream of clauses that is propositionally
 * equi-satisfiable with the conjunction of the formulas.
 * This stream is maintained in an online fashion.
 *
 * Unlike other parts of the system it is aware of the PropEngine's
 * internals such as the representation and translation of [??? -Chris]
 */

#pragma once

#include <sstream>
#include <string>
#include <unordered_set>
#include <vector>

#include "cvc5_private.h"

namespace cvc5 {
namespace prop {

/**
 * Boolean values of the SAT solver.
 */
enum SatValue {
  SAT_VALUE_UNKNOWN,
  SAT_VALUE_TRUE,
  SAT_VALUE_FALSE
};

/** Helper function for inverting a SatValue */
inline SatValue invertValue(SatValue v)
{
  if(v == SAT_VALUE_UNKNOWN) return SAT_VALUE_UNKNOWN;
  else if(v == SAT_VALUE_TRUE) return SAT_VALUE_FALSE;
  else return SAT_VALUE_TRUE;
}


/**
 * A variable of the SAT solver.
 */
typedef uint64_t SatVariable;

/**
 * Undefined SAT solver variable.
 */
const SatVariable undefSatVariable = SatVariable(-1);

/**
 * A SAT literal is a variable or an negated variable.
 */
class SatLiteral {

  /**
   * The value holds the variable and a bit noting if the variable is negated.
   */
  uint64_t d_value;

public:

  /**
   * Construct an undefined SAT literal.
   */
  SatLiteral()
  : d_value(undefSatVariable)
  {}

  /**
   * Construct a literal given a possible negated variable.
   */
  SatLiteral(SatVariable var, bool negated = false) {
    d_value = var + var + (int)negated;
  }

  /**
   * Returns the variable of the literal.
   */
  SatVariable getSatVariable() const {
    return d_value >> 1;
  }

  /**
   * Returns true if the literal is a negated variable.
   */
  bool isNegated() const {
    return d_value & 1;
  }

  /**
   * Negate the given literal.
   */
  SatLiteral operator ~ () const {
    return SatLiteral(getSatVariable(), !isNegated());
  }

  /**
   * Compare two literals for equality.
   */
  bool operator == (const SatLiteral& other) const {
    return d_value == other.d_value;
  }

  /**
   * Compare two literals for dis-equality.
   */
  bool operator != (const SatLiteral& other) const {
    return !(*this == other);
  }

  /**
   * Compare two literals
   */
  bool operator<(const SatLiteral& other) const
  {
    return getSatVariable() == other.getSatVariable()
               ? isNegated() < other.isNegated()
               : getSatVariable() < other.getSatVariable();
  }

  /**
   * Returns a string representation of the literal.
   */
  std::string toString() const {
    std::ostringstream os;
    os << (isNegated() ? "~" : "") << getSatVariable();
    return os.str();
  }

  /**
   * Returns the hash value of a literal.
   */
  size_t hash() const {
    return (size_t)d_value;
  }

  uint64_t toInt() const {
    return d_value;
  }

  /**
   * Returns true if the literal is undefined.
   */
  bool isNull() const {
    return getSatVariable() == undefSatVariable;
  }
};

/**
 * A constant representing a undefined literal.
 */
const SatLiteral undefSatLiteral = SatLiteral(undefSatVariable);

/**
 * Helper for hashing the literals.
 */
struct SatLiteralHashFunction {
  inline size_t operator() (const SatLiteral& literal) const {
    return literal.hash();
  }
};

/**
 * A SAT clause is a vector of literals.
 */
typedef std::vector<SatLiteral> SatClause;

struct SatClauseSetHashFunction
{
  inline size_t operator()(
      const std::unordered_set<SatLiteral, SatLiteralHashFunction>& clause)
      const
  {
    size_t acc = 0;
    for (const auto& l : clause)
    {
      acc ^= l.hash();
    }
    return acc;
  }
};

struct SatClauseLessThan
{
  bool operator()(const SatClause& l, const SatClause& r) const;
};

/**
 * Each object in the SAT solver, such as as variables and clauses, can be assigned a life span,
 * so that the SAT solver can (or should) remove them when the lifespan is over.
 */
enum SatSolverLifespan
{
  /**
   * The object should stay forever and never be removed
   */
  SAT_LIFESPAN_PERMANENT,
  /**
   * The object can be removed at any point when it becomes unnecessary.
   */
  SAT_LIFESPAN_REMOVABLE,
  /**
   * The object must be removed as soon as the SAT solver exits the search context
   * where the object got introduced.
   */
  SAT_LIFESPAN_SEARCH_CONTEXT_STRICT,
  /**
   * The object can be removed when SAT solver exits the search context where the object
   * got introduced, but can be kept at the solver discretion.
   */
  SAT_LIFESPAN_SEARCH_CONTEXT_LENIENT,
  /**
   * The object must be removed as soon as the SAT solver exits the user-level context where
   * the object got introduced.
   */
  SAT_LIFESPAN_USER_CONTEXT_STRICT,
  /**
   * The object can be removed when the SAT solver exits the user-level context where
   * the object got introduced.
   */
  SAT_LIFESPAN_USER_CONTEXT_LENIENT
};

}
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Dejan Jovanovic, Alex Ozdemir, Liana Hadarean
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		* This class transforms a sequence of formulas into clauses.
14		*
15		* This class takes a sequence of formulas.
16		* It outputs a stream of clauses that is propositionally
17		* equi-satisfiable with the conjunction of the formulas.
18		* This stream is maintained in an online fashion.
19		*
20		* Unlike other parts of the system it is aware of the PropEngine's
21		* internals such as the representation and translation of [??? -Chris]
22		*/
23
24		#pragma once
25
26		#include <sstream>
27		#include <string>
28		#include <unordered_set>
29		#include <vector>
30
31		#include "cvc5_private.h"
32
33		namespace cvc5 {
34		namespace prop {
35
36		/**
37		* Boolean values of the SAT solver.
38		*/
39		enum SatValue {
40		SAT_VALUE_UNKNOWN,
41		SAT_VALUE_TRUE,
42		SAT_VALUE_FALSE
43		};
44
45		/** Helper function for inverting a SatValue */
46	10862564	inline SatValue invertValue(SatValue v)
47		{
48	10862564	if(v == SAT_VALUE_UNKNOWN) return SAT_VALUE_UNKNOWN;
49	10862564	else if(v == SAT_VALUE_TRUE) return SAT_VALUE_FALSE;
50	5301983	else return SAT_VALUE_TRUE;
51		}
52
53
54		/**
55		* A variable of the SAT solver.
56		*/
57		typedef uint64_t SatVariable;
58
59		/**
60		* Undefined SAT solver variable.
61		*/
62		const SatVariable undefSatVariable = SatVariable(-1);
63
64		/**
65		* A SAT literal is a variable or an negated variable.
66		*/
67		class SatLiteral {
68
69		/**
70		* The value holds the variable and a bit noting if the variable is negated.
71		*/
72		uint64_t d_value;
73
74		public:
75
76		/**
77		* Construct an undefined SAT literal.
78		*/
79	38649781	SatLiteral()
80	38649781	: d_value(undefSatVariable)
81	38649781	{}
82
83		/**
84		* Construct a literal given a possible negated variable.
85		*/
86	47890097	SatLiteral(SatVariable var, bool negated = false) {
87	47890097	d_value = var + var + (int)negated;
88	47890097	}
89
90		/**
91		* Returns the variable of the literal.
92		*/
93	97416630	SatVariable getSatVariable() const {
94	97416630	return d_value >> 1;
95		}
96
97		/**
98		* Returns true if the literal is a negated variable.
99		*/
100	86220949	bool isNegated() const {
101	86220949	return d_value & 1;
102		}
103
104		/**
105		* Negate the given literal.
106		*/
107	23627839	SatLiteral operator ~ () const {
108	23627839	return SatLiteral(getSatVariable(), !isNegated());
109		}
110
111		/**
112		* Compare two literals for equality.
113		*/
114	99466854	bool operator == (const SatLiteral& other) const {
115	99466854	return d_value == other.d_value;
116		}
117
118		/**
119		* Compare two literals for dis-equality.
120		*/
121	46576	bool operator != (const SatLiteral& other) const {
122	46576	return !(*this == other);
123		}
124
125		/**
126		* Compare two literals
127		*/
128	3195520	bool operator<(const SatLiteral& other) const
129		{
130	3195520	return getSatVariable() == other.getSatVariable()
131	6176472	? isNegated() < other.isNegated()
132	6176472	: getSatVariable() < other.getSatVariable();
133		}
134
135		/**
136		* Returns a string representation of the literal.
137		*/
138		std::string toString() const {
139		std::ostringstream os;
140		os << (isNegated() ? "~" : "") << getSatVariable();
141		return os.str();
142		}
143
144		/**
145		* Returns the hash value of a literal.
146		*/
147	64605224	size_t hash() const {
148	64605224	return (size_t)d_value;
149		}
150
151		uint64_t toInt() const {
152		return d_value;
153		}
154
155		/**
156		* Returns true if the literal is undefined.
157		*/
158		bool isNull() const {
159		return getSatVariable() == undefSatVariable;
160		}
161		};
162
163		/**
164		* A constant representing a undefined literal.
165		*/
166	354039	const SatLiteral undefSatLiteral = SatLiteral(undefSatVariable);
167
168		/**
169		* Helper for hashing the literals.
170		*/
171		struct SatLiteralHashFunction {
172	64605224	inline size_t operator() (const SatLiteral& literal) const {
173	64605224	return literal.hash();
174		}
175		};
176
177		/**
178		* A SAT clause is a vector of literals.
179		*/
180		typedef std::vector<SatLiteral> SatClause;
181
182		struct SatClauseSetHashFunction
183		{
184		inline size_t operator()(
185		const std::unordered_set<SatLiteral, SatLiteralHashFunction>& clause)
186		const
187		{
188		size_t acc = 0;
189		for (const auto& l : clause)
190		{
191		acc ^= l.hash();
192		}
193		return acc;
194		}
195		};
196
197		struct SatClauseLessThan
198		{
199		bool operator()(const SatClause& l, const SatClause& r) const;
200		};
201
202		/**
203		* Each object in the SAT solver, such as as variables and clauses, can be assigned a life span,
204		* so that the SAT solver can (or should) remove them when the lifespan is over.
205		*/
206		enum SatSolverLifespan
207		{
208		/**
209		* The object should stay forever and never be removed
210		*/
211		SAT_LIFESPAN_PERMANENT,
212		/**
213		* The object can be removed at any point when it becomes unnecessary.
214		*/
215		SAT_LIFESPAN_REMOVABLE,
216		/**
217		* The object must be removed as soon as the SAT solver exits the search context
218		* where the object got introduced.
219		*/
220		SAT_LIFESPAN_SEARCH_CONTEXT_STRICT,
221		/**
222		* The object can be removed when SAT solver exits the search context where the object
223		* got introduced, but can be kept at the solver discretion.
224		*/
225		SAT_LIFESPAN_SEARCH_CONTEXT_LENIENT,
226		/**
227		* The object must be removed as soon as the SAT solver exits the user-level context where
228		* the object got introduced.
229		*/
230		SAT_LIFESPAN_USER_CONTEXT_STRICT,
231		/**
232		* The object can be removed when the SAT solver exits the user-level context where
233		* the object got introduced.
234		*/
235		SAT_LIFESPAN_USER_CONTEXT_LENIENT
236		};
237
238		}
239		} // namespace cvc5