circt::IncrementalSATSolver Class Reference

Abstract interface for incremental SAT solvers with an IPASIR-style API. More...

#include <SATSolver.h>

Public Types
enum	Result : int { kSAT = 10 , kUNSAT = 20 , kUNKNOWN = 0 }

Public Member Functions
virtual	~IncrementalSATSolver ()=default
virtual void	add (int lit)=0
virtual void	assume (int lit)=0
virtual Result	solve ()=0
virtual int	val (int v) const =0
virtual void	reserveVars (int maxVar)

Detailed Description

Abstract interface for incremental SAT solvers with an IPASIR-style API.

Definition at line 21 of file SATSolver.h.

Member Enumeration Documentation

Result

enum circt::IncrementalSATSolver::Result : int

Enumerator
kSAT
kUNSAT
kUNKNOWN

Definition at line 23 of file SATSolver.h.

Constructor & Destructor Documentation

~IncrementalSATSolver()

virtual circt::IncrementalSATSolver::~IncrementalSATSolver ( )

virtualdefault

Member Function Documentation

add()

virtual void circt::IncrementalSATSolver::add ( int  lit )

pure virtual

assume()

virtual void circt::IncrementalSATSolver::assume ( int  lit )

pure virtual

reserveVars()

virtual void circt::IncrementalSATSolver::reserveVars ( int  maxVar )

inlinevirtual

Definition at line 32 of file SATSolver.h.

solve()

virtual Result circt::IncrementalSATSolver::solve ( )

pure virtual

val()

virtual int circt::IncrementalSATSolver::val ( int  v ) const

pure virtual

---

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

• /home/runner/work/circt-www/circt-www/circt_src/include/circt/Support/SATSolver.h