AbstractModel (JavaSMT Solver Library)

java.lang.Object
- org.sosy_lab.java_smt.basicimpl.AbstractEvaluator<TFormulaInfo,TType,TEnv>
- - org.sosy_lab.java_smt.basicimpl.AbstractModel<TFormulaInfo,TType,TEnv>

All Implemented Interfaces:: AutoCloseable, Iterable<Model.ValueAssignment>, Evaluator, Model

public abstract class AbstractModel<TFormulaInfo,TType,TEnv>
extends AbstractEvaluator<TFormulaInfo,TType,TEnv>
implements Model

- Nested Class Summary
  - Nested classes/interfaces inherited from interface org.sosy_lab.java_smt.api.Model
    Model.ValueAssignment
- Field Summary
  - Fields inherited from class org.sosy_lab.java_smt.basicimpl.AbstractEvaluator
    creator
- Constructor Summary
  
  Constructors
  Modifier Constructor Description
  
  protected AbstractModel(AbstractProver<?> prover, FormulaCreator<TFormulaInfo,TType,TEnv,?> creator)
- Method Summary
  
  All Methods Instance Methods Concrete Methods
  Modifier and Type Method Description
  
  String toString()
  Pretty-printing of the model values.
  - Methods inherited from class org.sosy_lab.java_smt.basicimpl.AbstractEvaluator
    close, eval, evalImpl, evaluate, evaluate, evaluate, evaluate, evaluate, evaluate, evaluate, evaluate, evaluateImpl, isClosed
  - Methods inherited from class java.lang.Object
    clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
  - Methods inherited from interface org.sosy_lab.java_smt.api.Evaluator
    eval, evaluate, evaluate, evaluate, evaluate, evaluate, evaluate, evaluate, evaluate
  - Methods inherited from interface java.lang.Iterable
    forEach, spliterator
  - Methods inherited from interface org.sosy_lab.java_smt.api.Model
    asList, close, iterator

- Constructor Detail
  - AbstractModel
```
protected AbstractModel(AbstractProver<?> prover,
                        FormulaCreator<TFormulaInfo,TType,TEnv,?> creator)
```
- Method Detail
  - toString
```
public String toString()
```
    Description copied from interface: Model
    
    Pretty-printing of the model values.
    Please only use this method for debugging and not for retrieving relevant information about the model. The returned model representation is not intended for further usage like parsing, because we do not guarantee any specific format, e.g., for arrays and uninterpreted functions, and we allow the SMT solver to include arbitrary additional information about the current solver state, e.g., any available symbol in the solver, even from other provers, and temporary internal symbols.
    
    Specified by:
    
    toString in interface Model
    
    Overrides:
    
    toString in class Object