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
	Add one literal to the clause currently under construction.
virtual void	assume (int lit)=0
	Add an assumption literal for the next solve() call only.
virtual Result	solve ()=0
	Solve under the previously added clauses and current assumptions.
virtual Result	solve (llvm::ArrayRef< int > assumptions)
virtual int	val (int v) const =0
	Return the satisfying assignment for variable v from the last SAT result.
virtual void	setConflictLimit (int limit)
	Set the per-solve() conflict budget.
virtual void	reserveVars (int maxVar)
	Reserve storage for variables in the range [1, maxVar].
virtual void	addClause (llvm::ArrayRef< int > lits)
	Add a complete clause in one call.

Detailed Description

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

Definition at line 156 of file SATSolver.h.

Member Enumeration Documentation

Result

enum circt::IncrementalSATSolver::Result : int

Enumerator
kSAT
kUNSAT
kUNKNOWN

Definition at line 158 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

Add one literal to the clause currently under construction.

A 0 literal terminates the clause and submits it to the solver.

Referenced by addClause().

addClause()

virtual void circt::IncrementalSATSolver::addClause ( llvm::ArrayRef< int >  lits )

inlinevirtual

Add a complete clause in one call.

Definition at line 186 of file SATSolver.h.

References add().

assume()

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

pure virtual

Add an assumption literal for the next solve() call only.

Referenced by solve().

reserveVars()

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

inlinevirtual

Reserve storage for variables in the range [1, maxVar].

Definition at line 184 of file SATSolver.h.

setConflictLimit()

virtual void circt::IncrementalSATSolver::setConflictLimit ( int  limit )

inlinevirtual

Set the per-solve() conflict budget.

Negative values restore the backend default of no explicit conflict limit. The backend may choose to ignore this if it does not support conflict limits.

Definition at line 182 of file SATSolver.h.

solve() [1/2]

virtual Result circt::IncrementalSATSolver::solve ( )

pure virtual

Solve under the previously added clauses and current assumptions.

Referenced by solve().

solve() [2/2]

virtual Result circt::IncrementalSATSolver::solve ( llvm::ArrayRef< int >  assumptions )

inlinevirtual

Definition at line 169 of file SATSolver.h.

References assume(), and solve().

val()

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

pure virtual

Return the satisfying assignment for variable v from the last SAT result.

The sign of the returned literal encodes the Boolean value.

---

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