Package net.sf.tweety.logics.qbf.reasoner

Class CadetSolver

java.lang.Object

net.sf.tweety.logics.qbf.reasoner.QbfSolver

net.sf.tweety.logics.qbf.reasoner.CadetSolver

All Implemented Interfaces:

BeliefSetConsistencyTester<PlFormula>, ConsistencyTester<BeliefSet<PlFormula,?>>

public class CadetSolver
extends QbfSolver

A wrapper for the Cadet (https://markusrabe.github.io/cadet/) solver. Tested with version 2.5.

Author:

Anna Gessler

Field Summary

Fields

Modifier and Type	Field	Description
private java.lang.String	binaryLocation	String representation of the Cadet binary path.

Fields inherited from class net.sf.tweety.logics.qbf.reasoner.QbfSolver

bash

Constructor Summary

Constructors

Constructor	Description
CadetSolver(java.lang.String binaryLocation)	Constructs a new instance pointing to a specific CadetSolver
CadetSolver(java.lang.String binaryLocation, Shell bash)	Constructs a new instance pointing to a specific CadetSolver.

Method Summary

Modifier and Type	Method	Description
private boolean	evaluate(java.io.File file)	Invokes Cadet with the given input file.
boolean	isSatisfiable(java.util.Collection<PlFormula> kb)	Checks whether the given set of formulas is satisfiable.

Methods inherited from class net.sf.tweety.logics.qbf.reasoner.QbfSolver

isConsistent, isConsistent, isConsistent

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

binaryLocation

private java.lang.String binaryLocation

String representation of the Cadet binary path.

Constructor Detail

CadetSolver

public CadetSolver(java.lang.String binaryLocation,
                   Shell bash)

Constructs a new instance pointing to a specific CadetSolver.

Parameters:

binaryLocation - of the GhostQ executable on the hard drive

bash - shell to run commands

CadetSolver

public CadetSolver(java.lang.String binaryLocation)

Constructs a new instance pointing to a specific CadetSolver

Parameters:

binaryLocation - of the CadetSolver executable on the hard drive

Method Detail

evaluate

private boolean evaluate(java.io.File file)
                  throws java.lang.Exception

Invokes Cadet with the given input file.

Parameters:

file - input file for Cadet

Returns:

true if the result is SAT, false if the result is UNSAT

Throws:

java.lang.Exception - if the bash command fails or if Cadet produces no interpretable output

isSatisfiable

public boolean isSatisfiable(java.util.Collection<PlFormula> kb)

Description copied from class: QbfSolver

Checks whether the given set of formulas is satisfiable.

Specified by:

isSatisfiable in class QbfSolver

Parameters:

kb - a set of formulas.

Returns:

"true" if the set is consistent.