TheorySolver Class Reference

Theory solver for nonlinear theory over the Reals. More...

#include </home/soonhokong/work/dreal4/dreal/solver/theory_solver.h>

Public Member Functions
	TheorySolver (const Config &config)
bool	CheckSat (const Box &box, const std::vector< Formula > &assertions)
	Checks consistency. More...
const Box &	GetModel () const
	Gets a satisfying Model.
const std::set< Formula > &	GetExplanation () const
	Gets a list of used constraints.

Detailed Description

Theory solver for nonlinear theory over the Reals.

Member Function Documentation

CheckSat()

bool CheckSat	(	const Box &	box,
		const std::vector< Formula > &	assertions
	)

Checks consistency.

Returns true if there is a satisfying assignment. Otherwise, return false.

---

The documentation for this class was generated from the following files:

• /home/soonhokong/work/dreal4/dreal/solver/theory_solver.h
• /home/soonhokong/work/dreal4/dreal/solver/theory_solver.cc