Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/prop/sat_solver.h	Lines:	6	40	15.0 %
Date:	2021-05-22	Branches:	0	30	0.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Dejan Jovanovic, Liana Hadarean, Mathias Preiner
 *
 * 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.
 * ****************************************************************************
 *
 * SAT Solver.
 */

#include "cvc5_private.h"

#ifndef CVC5__PROP__SAT_SOLVER_H
#define CVC5__PROP__SAT_SOLVER_H

#include <string>

#include "context/cdlist.h"
#include "context/context.h"
#include "expr/node.h"
#include "expr/proof_node_manager.h"
#include "proof/clause_id.h"
#include "prop/bv_sat_solver_notify.h"
#include "prop/sat_solver_types.h"
#include "util/statistics_stats.h"

namespace cvc5 {

namespace prop {

class TheoryProxy;

class SatSolver {

public:

  /** Virtual destructor */
  virtual ~SatSolver() { }

  /** Assert a clause in the solver. */
  virtual ClauseId addClause(SatClause& clause,
                             bool removable) = 0;

  /** Return true if the solver supports native xor resoning */
  virtual bool nativeXor() { return false; }

  /** Add a clause corresponding to rhs = l1 xor .. xor ln  */
  virtual ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) = 0;

  /**
   * Create a new boolean variable in the solver.
   * @param isTheoryAtom is this a theory atom that needs to be asserted to theory
   * @param preRegister whether to preregister the atom with the theory
   * @param canErase whether the sat solver can safely eliminate this variable
   *
   */
  virtual SatVariable newVar(bool isTheoryAtom, bool preRegister, bool canErase) = 0;

  /** Create a new (or return an existing) boolean variable representing the constant true */
  virtual SatVariable trueVar() = 0;

  /** Create a new (or return an existing) boolean variable representing the constant false */
  virtual SatVariable falseVar() = 0;

  /** Check the satisfiability of the added clauses */
  virtual SatValue solve() = 0;

  /** Check the satisfiability of the added clauses */
  virtual SatValue solve(long unsigned int&) = 0;

  /** Check satisfiability under assumptions */
  virtual SatValue solve(const std::vector<SatLiteral>& assumptions)
  {
    Unimplemented() << "Solving under assumptions not implemented";
    return SAT_VALUE_UNKNOWN;
  };

  /**
   * Tell SAT solver to only do propagation on next solve().
   *
   * @return true if feature is supported, otherwise false.
   */
  virtual bool setPropagateOnly() { return false; }

  /** Interrupt the solver */
  virtual void interrupt() = 0;

  /** Call value() during the search.*/
  virtual SatValue value(SatLiteral l) = 0;

  /** Call modelValue() when the search is done.*/
  virtual SatValue modelValue(SatLiteral l) = 0;

  /** Get the current assertion level */
  virtual unsigned getAssertionLevel() const = 0;

  /** Check if the solver is in an inconsistent state */
  virtual bool ok() const = 0;

  /**
   * Get list of unsatisfiable assumptions.
   *
   * The returned assumptions are a subset of the assumptions provided to
   * the solve method.
   * Can only be called if satisfiability check under assumptions was used and
   * if it returned SAT_VALUE_FALSE.
   */
  virtual void getUnsatAssumptions(std::vector<SatLiteral>& unsat_assumptions)
  {
    Unimplemented() << "getUnsatAssumptions not implemented";
  }

};/* class SatSolver */


class BVSatSolverInterface: public SatSolver {
public:

  virtual ~BVSatSolverInterface() {}
  /** Interface for notifications */

  virtual void setNotify(BVSatSolverNotify* notify) = 0;

  virtual void markUnremovable(SatLiteral lit) = 0;

  virtual void getUnsatCore(SatClause& unsatCore) = 0;

  virtual void addMarkerLiteral(SatLiteral lit) = 0;

  virtual SatValue propagate() = 0;

  virtual void explain(SatLiteral lit, std::vector<SatLiteral>& explanation) = 0;

  virtual SatValue assertAssumption(SatLiteral lit, bool propagate = false) = 0;

  virtual void popAssumption() = 0;

};/* class BVSatSolverInterface */

class CDCLTSatSolverInterface : public SatSolver
{
 public:
  virtual ~CDCLTSatSolverInterface(){};

  virtual void initialize(context::Context* context,
                          prop::TheoryProxy* theoryProxy,
                          cvc5::context::UserContext* userContext,
                          ProofNodeManager* pnm) = 0;

  virtual void push() = 0;

  virtual void pop() = 0;

  /*
   * Reset the decisions in the DPLL(T) SAT solver at the current assertion
   * level.
   */
  virtual void resetTrail() = 0;

  virtual bool properExplanation(SatLiteral lit, SatLiteral expl) const = 0;

  virtual void requirePhase(SatLiteral lit) = 0;

  virtual bool isDecision(SatVariable decn) const = 0;

  /**
   * Return the current decision level of `lit`.
   */
  virtual int32_t getDecisionLevel(SatVariable v) const { return -1; }

  /**
   * Return the user-context level when `lit` was introduced..
   */
  virtual int32_t getIntroLevel(SatVariable v) const { return -1; }

  virtual std::shared_ptr<ProofNode> getProof() = 0;

}; /* class CDCLTSatSolverInterface */

inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) {
  out << lit.toString();
  return out;
}

inline std::ostream& operator <<(std::ostream& out, const prop::SatClause& clause) {
  out << "clause:";
  for(unsigned i = 0; i < clause.size(); ++i) {
    out << " " << clause[i];
  }
  out << ";";
  return out;
}

inline std::ostream& operator <<(std::ostream& out, prop::SatValue val) {
  std::string str;
  switch(val) {
  case prop::SAT_VALUE_UNKNOWN:
    str = "_";
    break;
  case prop::SAT_VALUE_TRUE:
    str = "1";
    break;
  case prop::SAT_VALUE_FALSE:
    str = "0";
    break;
  default:
    str = "Error";
    break;
  }

  out << str;
  return out;
}

}  // namespace prop
}  // namespace cvc5

#endif /* CVC5__PROP__SAT_MODULE_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Dejan Jovanovic, Liana Hadarean, Mathias Preiner
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		* SAT Solver.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__PROP__SAT_SOLVER_H
19		#define CVC5__PROP__SAT_SOLVER_H
20
21		#include <string>
22
23		#include "context/cdlist.h"
24		#include "context/context.h"
25		#include "expr/node.h"
26		#include "expr/proof_node_manager.h"
27		#include "proof/clause_id.h"
28		#include "prop/bv_sat_solver_notify.h"
29		#include "prop/sat_solver_types.h"
30		#include "util/statistics_stats.h"
31
32		namespace cvc5 {
33
34		namespace prop {
35
36		class TheoryProxy;
37
38	18952	class SatSolver {
39
40		public:
41
42		/** Virtual destructor */
43	18952	virtual ~SatSolver() { }
44
45		/** Assert a clause in the solver. */
46		virtual ClauseId addClause(SatClause& clause,
47		bool removable) = 0;
48
49		/** Return true if the solver supports native xor resoning */
50		virtual bool nativeXor() { return false; }
51
52		/** Add a clause corresponding to rhs = l1 xor .. xor ln */
53		virtual ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) = 0;
54
55		/**
56		* Create a new boolean variable in the solver.
57		* @param isTheoryAtom is this a theory atom that needs to be asserted to theory
58		* @param preRegister whether to preregister the atom with the theory
59		* @param canErase whether the sat solver can safely eliminate this variable
60		*
61		*/
62		virtual SatVariable newVar(bool isTheoryAtom, bool preRegister, bool canErase) = 0;
63
64		/** Create a new (or return an existing) boolean variable representing the constant true */
65		virtual SatVariable trueVar() = 0;
66
67		/** Create a new (or return an existing) boolean variable representing the constant false */
68		virtual SatVariable falseVar() = 0;
69
70		/** Check the satisfiability of the added clauses */
71		virtual SatValue solve() = 0;
72
73		/** Check the satisfiability of the added clauses */
74		virtual SatValue solve(long unsigned int&) = 0;
75
76		/** Check satisfiability under assumptions */
77		virtual SatValue solve(const std::vector<SatLiteral>& assumptions)
78		{
79		Unimplemented() << "Solving under assumptions not implemented";
80		return SAT_VALUE_UNKNOWN;
81		};
82
83		/**
84		* Tell SAT solver to only do propagation on next solve().
85		*
86		* @return true if feature is supported, otherwise false.
87		*/
88		virtual bool setPropagateOnly() { return false; }
89
90		/** Interrupt the solver */
91		virtual void interrupt() = 0;
92
93		/** Call value() during the search.*/
94		virtual SatValue value(SatLiteral l) = 0;
95
96		/** Call modelValue() when the search is done.*/
97		virtual SatValue modelValue(SatLiteral l) = 0;
98
99		/** Get the current assertion level */
100		virtual unsigned getAssertionLevel() const = 0;
101
102		/** Check if the solver is in an inconsistent state */
103		virtual bool ok() const = 0;
104
105		/**
106		* Get list of unsatisfiable assumptions.
107		*
108		* The returned assumptions are a subset of the assumptions provided to
109		* the solve method.
110		* Can only be called if satisfiability check under assumptions was used and
111		* if it returned SAT_VALUE_FALSE.
112		*/
113		virtual void getUnsatAssumptions(std::vector<SatLiteral>& unsat_assumptions)
114		{
115		Unimplemented() << "getUnsatAssumptions not implemented";
116		}
117
118		};/* class SatSolver */
119
120
121	9422	class BVSatSolverInterface: public SatSolver {
122		public:
123
124	9422	virtual ~BVSatSolverInterface() {}
125		/** Interface for notifications */
126
127		virtual void setNotify(BVSatSolverNotify* notify) = 0;
128
129		virtual void markUnremovable(SatLiteral lit) = 0;
130
131		virtual void getUnsatCore(SatClause& unsatCore) = 0;
132
133		virtual void addMarkerLiteral(SatLiteral lit) = 0;
134
135		virtual SatValue propagate() = 0;
136
137		virtual void explain(SatLiteral lit, std::vector<SatLiteral>& explanation) = 0;
138
139		virtual SatValue assertAssumption(SatLiteral lit, bool propagate = false) = 0;
140
141		virtual void popAssumption() = 0;
142
143		};/* class BVSatSolverInterface */
144
145	9494	class CDCLTSatSolverInterface : public SatSolver
146		{
147		public:
148	9494	virtual ~CDCLTSatSolverInterface(){};
149
150		virtual void initialize(context::Context* context,
151		prop::TheoryProxy* theoryProxy,
152		cvc5::context::UserContext* userContext,
153		ProofNodeManager* pnm) = 0;
154
155		virtual void push() = 0;
156
157		virtual void pop() = 0;
158
159		/*
160		* Reset the decisions in the DPLL(T) SAT solver at the current assertion
161		* level.
162		*/
163		virtual void resetTrail() = 0;
164
165		virtual bool properExplanation(SatLiteral lit, SatLiteral expl) const = 0;
166
167		virtual void requirePhase(SatLiteral lit) = 0;
168
169		virtual bool isDecision(SatVariable decn) const = 0;
170
171		/**
172		* Return the current decision level of `lit`.
173		*/
174		virtual int32_t getDecisionLevel(SatVariable v) const { return -1; }
175
176		/**
177		* Return the user-context level when `lit` was introduced..
178		*/
179		virtual int32_t getIntroLevel(SatVariable v) const { return -1; }
180
181		virtual std::shared_ptr<ProofNode> getProof() = 0;
182
183		}; /* class CDCLTSatSolverInterface */
184
185		inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) {
186		out << lit.toString();
187		return out;
188		}
189
190		inline std::ostream& operator <<(std::ostream& out, const prop::SatClause& clause) {
191		out << "clause:";
192		for(unsigned i = 0; i < clause.size(); ++i) {
193		out << " " << clause[i];
194		}
195		out << ";";
196		return out;
197		}
198
199		inline std::ostream& operator <<(std::ostream& out, prop::SatValue val) {
200		std::string str;
201		switch(val) {
202		case prop::SAT_VALUE_UNKNOWN:
203		str = "_";
204		break;
205		case prop::SAT_VALUE_TRUE:
206		str = "1";
207		break;
208		case prop::SAT_VALUE_FALSE:
209		str = "0";
210		break;
211		default:
212		str = "Error";
213		break;
214		}
215
216		out << str;
217		return out;
218		}
219
220		} // namespace prop
221		} // namespace cvc5
222
223		#endif /* CVC5__PROP__SAT_MODULE_H */