This makes symbol manager be in charge of determining which sorts and terms to print in response to get-model. This eliminates the need for the parser to call ExprManager::mkVar (and similar methods) with custom flags.
This requires significant simplifications to the printers for models, where instead of a NodeCommand, we take a Sort or Term to print in the model.
This is one of the last remaining steps for migrating the parser to the new API.
The next step will be to remove a lot of the internal infrastructure for managing expression names, commands to print in models, node commands, node listeners, etc.
api::Sort Parser::mkSort(const std::string& name, uint32_t flags)
{
Debug("parser") << "newSort(" << name << ")" << std::endl;
- api::Sort type =
- api::Sort(d_solver, d_solver->getExprManager()->mkSort(name, flags));
+ api::Sort type = d_solver->mkUninterpretedSort(name);
bool globalDecls = d_symman->getGlobalDeclarations();
defineType(
name, type, globalDecls && !(flags & ExprManager::SORT_FLAG_PLACEHOLDER));
{
Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")"
<< std::endl;
- api::Sort type = api::Sort(
- d_solver,
- d_solver->getExprManager()->mkSortConstructor(name, arity, flags));
+ api::Sort type = d_solver->mkSortConstructorSort(name, arity);
bool globalDecls = d_symman->getGlobalDeclarations();
defineType(name,
vector<api::Sort>(arity),
{
Debug("parser") << "newSortConstructor(P)(" << name << ", " << params.size()
<< ")" << std::endl;
- api::Sort unresolved =
- api::Sort(d_solver,
- d_solver->getExprManager()->mkSortConstructor(
- name, params.size(), ExprManager::SORT_FLAG_PLACEHOLDER));
+ api::Sort unresolved = d_solver->mkSortConstructorSort(name, params.size());
defineType(name, params, unresolved);
api::Sort t = getSort(name, params);
d_unresolved.insert(unresolved);
const api::Sort& type,
uint32_t flags)
{
- return api::Term(
- d_solver, d_solver->getExprManager()->mkVar(name, type.getType(), flags));
+ return d_solver->mkConst(type, name);
}
//!!!!!!!!!!! temporary
out << "Model()";
}
-void AstPrinter::toStream(std::ostream& out,
- const smt::Model& m,
- const NodeCommand* c) const
+void AstPrinter::toStreamModelSort(std::ostream& out,
+ const smt::Model& m,
+ TypeNode tn) const
+{
+ // shouldn't be called; only the non-Command* version above should be
+ Unreachable();
+}
+
+void AstPrinter::toStreamModelTerm(std::ostream& out,
+ const smt::Model& m,
+ Node n) const
{
// shouldn't be called; only the non-Command* version above should be
Unreachable();
}
void AstPrinter::toStreamCmdDeclareType(std::ostream& out,
- const std::string& id,
- size_t arity,
TypeNode type) const
{
- out << "DeclareType(" << id << "," << arity << "," << type << ')'
- << std::endl;
+ out << "DeclareType(" << type << ')' << std::endl;
}
void AstPrinter::toStreamCmdDefineType(std::ostream& out,
/** Print declare-sort command */
void toStreamCmdDeclareType(std::ostream& out,
- const std::string& id,
- size_t arity,
TypeNode type) const override;
/** Print define-sort command */
private:
void toStream(std::ostream& out, TNode n, int toDepth) const;
- void toStream(std::ostream& out,
- const smt::Model& m,
- const NodeCommand* c) const override;
+ /**
+ * To stream model sort. This prints the appropriate output for type
+ * tn declared via declare-sort or declare-datatype.
+ */
+ void toStreamModelSort(std::ostream& out,
+ const smt::Model& m,
+ TypeNode tn) const override;
+
+ /**
+ * To stream model term. This prints the appropriate output for term
+ * n declared via declare-fun.
+ */
+ void toStreamModelTerm(std::ostream& out,
+ const smt::Model& m,
+ Node n) const override;
}; /* class AstPrinter */
} // namespace ast
}/* CvcPrinter::toStream(CommandStatus*) */
-namespace {
-
-void DeclareTypeNodeCommandToStream(std::ostream& out,
- const theory::TheoryModel& model,
- const DeclareTypeNodeCommand& command)
+void CvcPrinter::toStreamModelSort(std::ostream& out,
+ const smt::Model& m,
+ TypeNode tn) const
{
- TypeNode type_node = command.getType();
- const std::vector<Node>* type_reps =
- model.getRepSet()->getTypeRepsOrNull(type_node);
+ if (!tn.isSort())
+ {
+ out << "ERROR: don't know how to print a non uninterpreted sort in model: "
+ << tn << std::endl;
+ return;
+ }
+ const theory::TheoryModel* tm = m.getTheoryModel();
+ const std::vector<Node>* type_reps = tm->getRepSet()->getTypeRepsOrNull(tn);
if (options::modelUninterpPrint() == options::ModelUninterpPrintMode::DtEnum
- && type_node.isSort() && type_reps != nullptr)
+ && type_reps != nullptr)
{
out << "DATATYPE" << std::endl;
- out << " " << command.getSymbol() << " = ";
+ out << " " << tn << " = ";
for (size_t i = 0; i < type_reps->size(); i++)
{
if (i > 0)
}
out << std::endl << "END;" << std::endl;
}
- else if (type_node.isSort() && type_reps != nullptr)
+ else if (type_reps != nullptr)
{
- out << "% cardinality of " << type_node << " is " << type_reps->size()
+ out << "% cardinality of " << tn << " is " << type_reps->size()
<< std::endl;
- out << command << std::endl;
+ toStreamCmdDeclareType(out, tn);
for (Node type_rep : *type_reps)
{
if (type_rep.isVar())
{
- out << type_rep << " : " << type_node << ";" << std::endl;
+ out << type_rep << " : " << tn << ";" << std::endl;
}
else
{
}
else
{
- out << command << std::endl;
+ toStreamCmdDeclareType(out, tn);
}
}
-void DeclareFunctionNodeCommandToStream(
- std::ostream& out,
- const theory::TheoryModel& model,
- const DeclareFunctionNodeCommand& command)
+void CvcPrinter::toStreamModelTerm(std::ostream& out,
+ const smt::Model& m,
+ Node n) const
{
- Node n = command.getFunction();
- if (n.getKind() == kind::SKOLEM)
- {
- // don't print out internal stuff
- return;
- }
+ const theory::TheoryModel* tm = m.getTheoryModel();
TypeNode tn = n.getType();
out << n << " : ";
if (tn.isFunction() || tn.isPredicate())
}
// We get the value from the theory model directly, which notice
// does not have to go through the standard SmtEngine::getValue interface.
- Node val = model.getValue(n);
+ Node val = tm->getValue(n);
if (options::modelUninterpPrint() == options::ModelUninterpPrintMode::DtEnum
&& val.getKind() == kind::STORE)
{
TypeNode type_node = val[1].getType();
if (tn.isSort())
{
- if (const std::vector<Node>* type_reps =
- model.getRepSet()->getTypeRepsOrNull(type_node))
+ const std::vector<Node>* type_reps =
+ tm->getRepSet()->getTypeRepsOrNull(type_node);
+ if (type_reps != nullptr)
{
Cardinality indexCard(type_reps->size());
val = theory::arrays::TheoryArraysRewriter::normalizeConstant(
out << " = " << val << ";" << std::endl;
}
-} // namespace
-
void CvcPrinter::toStream(std::ostream& out, const smt::Model& m) const
{
const theory::TheoryModel* tm = m.getTheoryModel();
out << "MODEL END;" << std::endl;
}
-void CvcPrinter::toStream(std::ostream& out,
- const smt::Model& model,
- const NodeCommand* command) const
-{
- const auto* theory_model = model.getTheoryModel();
- AlwaysAssert(theory_model != nullptr);
- if (const auto* declare_type_command =
- dynamic_cast<const DeclareTypeNodeCommand*>(command))
- {
- DeclareTypeNodeCommandToStream(out, *theory_model, *declare_type_command);
- }
- else if (const auto* dfc =
- dynamic_cast<const DeclareFunctionNodeCommand*>(command))
- {
- DeclareFunctionNodeCommandToStream(out, *theory_model, *dfc);
- }
- else
- {
- out << *command << std::endl;
- }
-}
-
void CvcPrinter::toStreamCmdAssert(std::ostream& out, Node n) const
{
out << "ASSERT " << n << ';' << std::endl;
{
DeclarationDefinitionCommand* dd =
static_cast<DeclarationDefinitionCommand*>(*i++);
+ Assert(dd != nullptr);
if (i != sequence.cend())
{
out << dd->getSymbol() << ", ";
}
void CvcPrinter::toStreamCmdDeclareType(std::ostream& out,
- const std::string& id,
- size_t arity,
TypeNode type) const
{
+ size_t arity = type.isSortConstructor() ? type.getSortConstructorArity() : 0;
if (arity > 0)
{
- // TODO?
out << "ERROR: Don't know how to print parameterized type declaration "
"in CVC language."
<< std::endl;
}
else
{
- out << id << " : TYPE;" << std::endl;
+ out << type << " : TYPE;" << std::endl;
}
}
/** Print declare-sort command */
void toStreamCmdDeclareType(std::ostream& out,
- const std::string& id,
- size_t arity,
TypeNode type) const override;
/** Print define-sort command */
private:
void toStream(std::ostream& out, TNode n, int toDepth, bool bracket) const;
- void toStream(std::ostream& out,
- const smt::Model& m,
- const NodeCommand* c) const override;
+ /**
+ * To stream model sort. This prints the appropriate output for type
+ * tn declared via declare-sort or declare-datatype.
+ */
+ void toStreamModelSort(std::ostream& out,
+ const smt::Model& m,
+ TypeNode tn) const override;
+
+ /**
+ * To stream model term. This prints the appropriate output for term
+ * n declared via declare-fun.
+ */
+ void toStreamModelTerm(std::ostream& out,
+ const smt::Model& m,
+ Node n) const override;
bool d_cvc3Mode;
}; /* class CvcPrinter */
void Printer::toStream(std::ostream& out, const smt::Model& m) const
{
- for(size_t i = 0; i < m.getNumCommands(); ++i) {
- const NodeCommand* cmd = m.getCommand(i);
- const DeclareFunctionNodeCommand* dfc =
- dynamic_cast<const DeclareFunctionNodeCommand*>(cmd);
- if (dfc != NULL && !m.isModelCoreSymbol(dfc->getFunction()))
+ // print the declared sorts
+ const std::vector<TypeNode>& dsorts = m.getDeclaredSorts();
+ for (const TypeNode& tn : dsorts)
+ {
+ toStreamModelSort(out, m, tn);
+ }
+
+ // print the declared terms
+ const std::vector<Node>& dterms = m.getDeclaredTerms();
+ for (const Node& n : dterms)
+ {
+ // take into account model core, independently of the format
+ if (!m.isModelCoreSymbol(n))
{
continue;
}
- toStream(out, m, cmd);
+ toStreamModelTerm(out, m, n);
}
+
}/* Printer::toStream(Model) */
+void Printer::toStreamUsing(OutputLanguage lang,
+ std::ostream& out,
+ const smt::Model& m) const
+{
+ getPrinter(lang)->toStream(out, m);
+}
+
void Printer::toStream(std::ostream& out, const UnsatCore& core) const
{
for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) {
}
void Printer::toStreamCmdDeclareType(std::ostream& out,
- const std::string& id,
- size_t arity,
TypeNode type) const
{
printUnknownCommand(out, "declare-sort");
/** Print declare-sort command */
virtual void toStreamCmdDeclareType(std::ostream& out,
- const std::string& id,
- size_t arity,
TypeNode type) const;
/** Print define-sort command */
/** Derived classes can construct, but no one else. */
Printer() {}
- /** write model response to command */
- virtual void toStream(std::ostream& out,
- const smt::Model& m,
- const NodeCommand* c) const = 0;
+ /**
+ * To stream model sort. This prints the appropriate output for type
+ * tn declared via declare-sort or declare-datatype.
+ */
+ virtual void toStreamModelSort(std::ostream& out,
+ const smt::Model& m,
+ TypeNode tn) const = 0;
+
+ /**
+ * To stream model term. This prints the appropriate output for term
+ * n declared via declare-fun.
+ */
+ virtual void toStreamModelTerm(std::ostream& out,
+ const smt::Model& m,
+ Node n) const = 0;
/** write model response to command using another language printer */
void toStreamUsing(OutputLanguage lang,
std::ostream& out,
- const smt::Model& m,
- const NodeCommand* c) const
- {
- getPrinter(lang)->toStream(out, m, c);
- }
+ const smt::Model& m) const;
/**
* Write an error to `out` stating that command `name` is not supported by
}
}
-void Smt2Printer::toStream(std::ostream& out,
- const smt::Model& model,
- const NodeCommand* command) const
+void Smt2Printer::toStreamModelSort(std::ostream& out,
+ const smt::Model& m,
+ TypeNode tn) const
{
- const theory::TheoryModel* theory_model = model.getTheoryModel();
- AlwaysAssert(theory_model != nullptr);
- if (const DeclareTypeNodeCommand* dtc =
- dynamic_cast<const DeclareTypeNodeCommand*>(command))
+ if (!tn.isSort())
{
- // print out the DeclareTypeCommand
- TypeNode tn = dtc->getType();
- if (!tn.isSort())
+ out << "ERROR: don't know how to print non uninterpreted sort in model: "
+ << tn << std::endl;
+ return;
+ }
+ const theory::TheoryModel* tm = m.getTheoryModel();
+ std::vector<Node> elements = tm->getDomainElements(tn);
+ if (options::modelUninterpPrint() == options::ModelUninterpPrintMode::DtEnum)
+ {
+ if (isVariant_2_6(d_variant))
{
- out << (*dtc) << endl;
+ out << "(declare-datatypes ((" << tn << " 0)) (";
}
else
{
- std::vector<Node> elements = theory_model->getDomainElements(tn);
- if (options::modelUninterpPrint()
- == options::ModelUninterpPrintMode::DtEnum)
- {
- if (isVariant_2_6(d_variant))
- {
- out << "(declare-datatypes ((" << (*dtc).getSymbol() << " 0)) (";
- }
- else
- {
- out << "(declare-datatypes () ((" << (*dtc).getSymbol() << " ";
- }
- for (const Node& type_ref : elements)
- {
- out << "(" << type_ref << ")";
- }
- out << ")))" << endl;
- }
- else
- {
- // print the cardinality
- out << "; cardinality of " << tn << " is " << elements.size() << endl;
- if (options::modelUninterpPrint()
- == options::ModelUninterpPrintMode::DeclSortAndFun)
- {
- out << (*dtc) << endl;
- }
- // print the representatives
- for (const Node& trn : elements)
- {
- if (trn.isVar())
- {
- out << "(declare-fun " << quoteSymbol(trn) << " () " << tn << ")"
- << endl;
- }
- else
- {
- out << "; rep: " << trn << endl;
- }
- }
- }
- }
- }
- else if (const DeclareFunctionNodeCommand* dfc =
- dynamic_cast<const DeclareFunctionNodeCommand*>(command))
- {
- // print out the DeclareFunctionCommand
- Node n = dfc->getFunction();
- if ((*dfc).getPrintInModelSetByUser())
- {
- if (!(*dfc).getPrintInModel())
- {
- return;
- }
+ out << "(declare-datatypes () ((" << tn << " ";
}
- else if (n.getKind() == kind::SKOLEM)
+ for (const Node& type_ref : elements)
{
- // don't print out internal stuff
- return;
+ out << "(" << type_ref << ")";
}
- // We get the value from the theory model directly, which notice
- // does not have to go through the standard SmtEngine::getValue interface.
- Node val = theory_model->getValue(n);
- if (val.getKind() == kind::LAMBDA)
+ out << ")))" << endl;
+ return;
+ }
+ // print the cardinality
+ out << "; cardinality of " << tn << " is " << elements.size() << endl;
+ if (options::modelUninterpPrint()
+ == options::ModelUninterpPrintMode::DeclSortAndFun)
+ {
+ toStreamCmdDeclareType(out, tn);
+ }
+ // print the representatives
+ for (const Node& trn : elements)
+ {
+ if (trn.isVar())
{
- TypeNode rangeType = n.getType().getRangeType();
- out << "(define-fun " << n << " " << val[0] << " " << rangeType << " ";
- // call toStream and force its type to be proper
- toStreamCastToType(out, val[1], -1, rangeType);
- out << ")" << endl;
+ out << "(declare-fun " << quoteSymbol(trn) << " () " << tn << ")" << endl;
}
else
{
- if (options::modelUninterpPrint()
- == options::ModelUninterpPrintMode::DtEnum
- && val.getKind() == kind::STORE)
- {
- TypeNode tn = val[1].getType();
- const std::vector<Node>* type_refs =
- theory_model->getRepSet()->getTypeRepsOrNull(tn);
- if (tn.isSort() && type_refs != nullptr)
- {
- Cardinality indexCard(type_refs->size());
- val = theory::arrays::TheoryArraysRewriter::normalizeConstant(
- val, indexCard);
- }
- }
- out << "(define-fun " << n << " () " << n.getType() << " ";
- // call toStream and force its type to be proper
- toStreamCastToType(out, val, -1, n.getType());
- out << ")" << endl;
+ out << "; rep: " << trn << endl;
}
}
- else if (const DeclareDatatypeNodeCommand* declare_datatype_command =
- dynamic_cast<const DeclareDatatypeNodeCommand*>(command))
+}
+
+void Smt2Printer::toStreamModelTerm(std::ostream& out,
+ const smt::Model& m,
+ Node n) const
+{
+ const theory::TheoryModel* tm = m.getTheoryModel();
+ // We get the value from the theory model directly, which notice
+ // does not have to go through the standard SmtEngine::getValue interface.
+ Node val = tm->getValue(n);
+ if (val.getKind() == kind::LAMBDA)
{
- out << *declare_datatype_command;
+ TypeNode rangeType = n.getType().getRangeType();
+ out << "(define-fun " << n << " " << val[0] << " " << rangeType << " ";
+ // call toStream and force its type to be proper
+ toStreamCastToType(out, val[1], -1, rangeType);
+ out << ")" << endl;
}
else
{
- Unreachable();
+ if (options::modelUninterpPrint() == options::ModelUninterpPrintMode::DtEnum
+ && val.getKind() == kind::STORE)
+ {
+ TypeNode tn = val[1].getType();
+ const std::vector<Node>* type_refs =
+ tm->getRepSet()->getTypeRepsOrNull(tn);
+ if (tn.isSort() && type_refs != nullptr)
+ {
+ Cardinality indexCard(type_refs->size());
+ val = theory::arrays::TheoryArraysRewriter::normalizeConstant(
+ val, indexCard);
+ }
+ }
+ out << "(define-fun " << n << " () " << n.getType() << " ";
+ // call toStream and force its type to be proper
+ toStreamCastToType(out, val, -1, n.getType());
+ out << ")" << endl;
}
}
}
void Smt2Printer::toStreamCmdDeclareType(std::ostream& out,
- const std::string& id,
- size_t arity,
TypeNode type) const
{
- out << "(declare-sort " << CVC4::quoteSymbol(id) << " " << arity << ")"
+ Assert(type.isSort() || type.isSortConstructor());
+ std::stringstream id;
+ id << type;
+ size_t arity = type.isSortConstructor() ? type.getSortConstructorArity() : 0;
+ out << "(declare-sort " << CVC4::quoteSymbol(id.str()) << " " << arity << ")"
<< std::endl;
}
/** Print declare-sort command */
void toStreamCmdDeclareType(std::ostream& out,
- const std::string& id,
- size_t arity,
TypeNode type) const override;
/** Print define-sort command */
TNode n,
int toDepth,
TypeNode tn) const;
- void toStream(std::ostream& out,
- const smt::Model& m,
- const NodeCommand* c) const override;
void toStream(std::ostream& out, const SExpr& sexpr) const;
void toStream(std::ostream& out, const DType& dt) const;
+ /**
+ * To stream model sort. This prints the appropriate output for type
+ * tn declared via declare-sort or declare-datatype.
+ */
+ void toStreamModelSort(std::ostream& out,
+ const smt::Model& m,
+ TypeNode tn) const override;
+
+ /**
+ * To stream model term. This prints the appropriate output for term
+ * n declared via declare-fun.
+ */
+ void toStreamModelTerm(std::ostream& out,
+ const smt::Model& m,
+ Node n) const override;
+
/**
* To stream with let binding. This prints n, possibly in the scope
* of letification generated by this method based on lbind.
: "CandidateFiniteModel");
out << "% SZS output start " << statusName << " for " << m.getInputName()
<< endl;
- for(size_t i = 0; i < m.getNumCommands(); ++i) {
- this->Printer::toStreamUsing(language::output::LANG_SMTLIB_V2_5, out, m, m.getCommand(i));
- }
+ this->Printer::toStreamUsing(language::output::LANG_SMTLIB_V2_5, out, m);
out << "% SZS output end " << statusName << " for " << m.getInputName()
<< endl;
}
-void TptpPrinter::toStream(std::ostream& out,
- const smt::Model& m,
- const NodeCommand* c) const
+void TptpPrinter::toStreamModelSort(std::ostream& out,
+ const smt::Model& m,
+ TypeNode tn) const
+{
+ // shouldn't be called; only the non-Command* version above should be
+ Unreachable();
+}
+
+void TptpPrinter::toStreamModelTerm(std::ostream& out,
+ const smt::Model& m,
+ Node n) const
{
// shouldn't be called; only the non-Command* version above should be
Unreachable();
}
+
void TptpPrinter::toStream(std::ostream& out, const UnsatCore& core) const
{
out << "% SZS output start UnsatCore " << std::endl;
void toStream(std::ostream& out, const UnsatCore& core) const override;
private:
- void toStream(std::ostream& out,
- const smt::Model& m,
- const NodeCommand* c) const override;
+ /**
+ * To stream model sort. This prints the appropriate output for type
+ * tn declared via declare-sort or declare-datatype.
+ */
+ void toStreamModelSort(std::ostream& out,
+ const smt::Model& m,
+ TypeNode tn) const override;
+
+ /**
+ * To stream model term. This prints the appropriate output for term
+ * n declared via declare-fun.
+ */
+ void toStreamModelTerm(std::ostream& out,
+ const smt::Model& m,
+ Node n) const override;
}; /* class TptpPrinter */
void DeclareFunctionCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
+ // mark that it will be printed in the model
+ sm->addModelDeclarationTerm(d_func);
d_commandStatus = CommandSuccess::instance();
}
api::Sort DeclareSortCommand::getSort() const { return d_sort; }
void DeclareSortCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
+ // mark that it will be printed in the model
+ sm->addModelDeclarationSort(d_sort);
d_commandStatus = CommandSuccess::instance();
}
size_t dag,
OutputLanguage language) const
{
- Printer::getPrinter(language)->toStreamCmdDeclareType(
- out, d_sort.toString(), d_arity, d_sort.getTypeNode());
+ Printer::getPrinter(language)->toStreamCmdDeclareType(out,
+ d_sort.getTypeNode());
}
/* -------------------------------------------------------------------------- */
try
{
d_result = solver->getSmtEngine()->getModel();
+ // set the model declarations, which determines what is printed in the model
+ d_result->clearModelDeclarations();
+ std::vector<api::Sort> declareSorts = sm->getModelDeclareSorts();
+ for (const api::Sort& s : declareSorts)
+ {
+ d_result->addDeclarationSort(s.getTypeNode());
+ }
+ std::vector<api::Term> declareTerms = sm->getModelDeclareTerms();
+ for (const api::Term& t : declareTerms)
+ {
+ d_result->addDeclarationTerm(t.getNode());
+ }
d_commandStatus = CommandSuccess::instance();
}
catch (RecoverableModalException& e)
size_t dag,
OutputLanguage language) const
{
- Printer::getPrinter(language)->toStreamCmdDeclareType(
- out, d_id, d_arity, d_type);
+ Printer::getPrinter(language)->toStreamCmdDeclareType(out, d_type);
}
NodeCommand* DeclareTypeNodeCommand::clone() const
; EXPECT: sat
; EXPECT: (
-; EXPECT: (declare-datatypes ((Pair 2)) ((par (X Y)((mkPair (first X) (second Y))))))
; EXPECT: (define-fun x () (Pair Int Real) ((as mkPair (Pair Int Real)) 2 (/ 3 2)))
; EXPECT: )
tryGoodInput("a : INT = 5; a: INT;"); // decl after define, compatible
tryGoodInput("a : TYPE; a : INT;"); // ok, sort and variable symbol spaces distinct
tryGoodInput("a : TYPE; a : INT; b : a;"); // ok except a is both INT and sort `a'
- //tryGoodInput("a : [0..0]; b : [-5..5]; c : [-1..1]; d : [ _ .._];"); // subranges
- tryGoodInput("a : [ _..1]; b : [_.. 0]; c :[_..-1];");
tryGoodInput("DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE cons = null END;");
tryGoodInput("DATATYPE tree = node(data:list), list = cons(car:tree,cdr:list) | nil END;");
//tryGoodInput("DATATYPE tree = node(data:[list,list,ARRAY tree OF list]), list = cons(car:ARRAY list OF tree,cdr:BITVECTOR(32)) END;");
projects / cvc5.git / commitdiff