P4::AbstractSolver Class Reference

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

#include <solver.h>

Inheritance diagram for P4::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 P4::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 P4::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 P4::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 > P4::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 P4::P4Tools::Z3Solver.

comment()

virtual void P4::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 P4::P4Tools::Z3Solver.

getSymbolicMapping()

virtual const SymbolicMapping & P4::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 P4::P4Tools::Z3Solver.

isInIncrementalMode()

virtual bool P4::AbstractSolver::isInIncrementalMode ( ) const

nodiscardpure virtual

Returns

whether this solver is incremental.

Implemented in P4::P4Tools::Z3Solver.

seed()

virtual void P4::AbstractSolver::seed ( unsigned seed )

pure virtual

Seeds the pseudo-random number generator in the solver. The solver's PRNG is used to randomize the models produced by @getModel.

Implemented in P4::P4Tools::Z3Solver.

timeout()

virtual void P4::AbstractSolver::timeout ( unsigned tm )

pure virtual

Sets timeout for solver in milliseconds.

Implemented in P4::P4Tools::Z3Solver.

toJSON()

virtual void P4::AbstractSolver::toJSON ( JSONGenerator & ) const

pure virtual

Saves solver state to the given JSON generator.

Implemented in P4::P4Tools::Z3Solver.