Provides a higher-level interface for an SMT solver. More...

#include <solver.h>

Inheritance diagram for AbstractSolver:

Public Member Functions
virtual std::optional< bool >	checkSat (const std::vector< const Constraint * > &asserts)=0

virtual void	comment (cstring comment)=0

	DECLARE_TYPEINFO (AbstractSolver)

virtual const SymbolicMapping &	getSymbolicMapping () const =0

virtual bool	isInIncrementalMode () const =0

virtual void	seed (unsigned seed)=0

virtual void	timeout (unsigned tm)=0
	Sets timeout for solver in milliseconds.

virtual void	toJSON (JSONGenerator &) const =0
	Saves solver state to the given JSON generator.

Public Member Functions inherited from ICastable
template<typename T >
T &	as ()
	Tries to convert the class to type T. A BUG occurs if the cast fails.

template<typename T >
const T &	as () const
	Tries to convert the class to type T. A BUG occurs if the cast fails.

template<typename T >
T *	checkedTo ()
	Performs a checked cast. A BUG occurs if the cast fails.

template<typename T >
const T *	checkedTo () const
	Performs a checked cast. A BUG occurs if the cast fails.

Public Member Functions inherited from RTTI::Base
template<typename T >
bool	is () const noexcept

virtual bool	isA (TypeId typeId) const noexcept=0

template<typename T >
const T *	to () const noexcept
	Same as `to`, but returns const pointer to T.

template<typename T >
T *	to () noexcept

virtual TypeId	typeId () const noexcept=0

Additional Inherited Members
Protected Member Functions inherited from RTTI::Base
virtual const void *	toImpl (TypeId typeId) const noexcept=0

Detailed Description

Provides a higher-level interface for an SMT solver.

Member Function Documentation

◆ checkSat()

virtual std::optional< bool > AbstractSolver::checkSat ( const std::vector< const Constraint * > & asserts )

pure virtual

Determines whether the set of assertions given to the solver are consistent.

Returns: true if the given assertions are consistent.; false if the given assertions are inconsistent.; std::nullopt if the solver times out, or is otherwise unable to provide an answer.

Implemented in P4Tools::Z3Solver.

◆ comment()

virtual void AbstractSolver::comment ( cstring comment )

pure virtual

Adds a comment to any log file that might be produced. Useful for understanding the sequence of calls made to the solver when debugging.

Implemented in P4Tools::Z3Solver.

◆ getSymbolicMapping()

virtual const SymbolicMapping & AbstractSolver::getSymbolicMapping ( ) const

nodiscardpure virtual

Obtains the first solution found by the solver in the last call to @checkSat.

A BUG occurs if the solver has no available solution. This can happen if the last call to @checkSat returned anything other than true, if there was no such previous call, or if the state in the solver has changed since the last such call (e.g., more assertions have been made).

Implemented in P4Tools::Z3Solver.