Skip to main content

module lang::smtlib2::command::response::Ast

rascal-0.40.16

Synopsis: Represents the AST of the SMT solver response.

Usage​

import lang::smtlib2::command::response::Ast;

data Response​

data Response  
     = response(CheckSat sat)
     | response(GetUnsatCore unsatCore)
     | response(GetValue model)
     | none()
     ;

data CheckSat​

data CheckSat  
     = sat()
     | unsat()
     | unknown()
     ;

data GetUnsatCore​

data GetUnsatCore  
     = unsatCore(list[str] labels)
     ;

data GetValue​

data GetValue  
     = foundValues(list[Model] models)
     ;

data Model​

data Model  
     = model(Expr var, Expr val)
     ;