From: Andres Noetzli Date: Thu, 31 Mar 2022 19:11:41 +0000 (-0700) Subject: Remove examples that use the old API (#8486) X-Git-Tag: cvc5-1.0.0~87 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=04d3abb9fe0ed0bc4f6fa5ff1976f91457c03a14;p=cvc5.git Remove examples that use the old API (#8486) This removes examples that use the old API and the parser. They were not currently being compiled and we can reintroduce them if we need them/have a new parser API. --- diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt index 27ecd72b5..a7dde9c77 100644 --- a/examples/CMakeLists.txt +++ b/examples/CMakeLists.txt @@ -73,15 +73,8 @@ endmacro() cvc5_add_example(simple_vc_cxx "" "") cvc5_add_example(simple_vc_quant_cxx "" "") -# TODO(project issue $206): Port example to new API -# cvc5_add_example(translator "" "" -# # argument to binary (for testing) -# ${CMAKE_CURRENT_SOURCE_DIR}/translator-example-input.smt2) add_subdirectory(api/cpp) -# TODO(project issue $206): Port example to new API -# add_subdirectory(nra-translate) -# add_subdirectory(sets-translate) if(TARGET cvc5::cvc5jar) find_package(Java REQUIRED) diff --git a/examples/nra-translate/CMakeLists.txt b/examples/nra-translate/CMakeLists.txt deleted file mode 100644 index dda47206e..000000000 --- a/examples/nra-translate/CMakeLists.txt +++ /dev/null @@ -1,37 +0,0 @@ -############################################################################### -# Top contributors (to current version): -# Aina Niemetz, Mathias Preiner -# -# This file is part of the cvc5 project. -# -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS -# in the top-level source directory and their institutional affiliations. -# All rights reserved. See the file COPYING in the top-level source -# directory for licensing information. -# ############################################################################# -# -# The build system configuration. -## - -set(EXAMPLES_NRA_TRANSLATE_BIN_DIR ${EXAMPLES_BIN_DIR}/nra-translate) - -set(CVC5_EXAMPLES_NRA_TRANSLATE - normalize - smt2info - smt2todreal - smt2toisat - smt2tomathematica - smt2toqepcad - smt2toredlog -) - -foreach(example ${CVC5_EXAMPLES_NRA_TRANSLATE}) - cvc5_add_example(${example} "" "nra-translate" - # arguments to binary (for testing) - # input file is required by all tests - ${CMAKE_CURRENT_SOURCE_DIR}/nra-translate-example-input.smt2 - # This is a dummy argument for smt2toredlog (argument is only printed, can - # be anything for testing purposes). We pass this to all examples since the - # other examples ignore additional arguments. - "foo") -endforeach() diff --git a/examples/nra-translate/normalize.cpp b/examples/nra-translate/normalize.cpp deleted file mode 100644 index 6a116d3d9..000000000 --- a/examples/nra-translate/normalize.cpp +++ /dev/null @@ -1,82 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Dejan Jovanovic, Aina Niemetz, Tim King - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * [[ Add one-line brief description here ]] - * - * [[ Add lengthier description here ]] - * \todo document this file - */ - -#include -#include -#include - -#include -#include -#include -#include -#include -#include - -using namespace std; -using namespace cvc5; -using namespace cvc5::parser; -using namespace cvc5::theory; - -int main(int argc, char* argv[]) -{ - - // Get the filename - string input(argv[1]); - - // Create the expression manager - Options options; - options.setInputLanguage(language::input::LANG_SMTLIB_V2); - std::unique_ptr solver = - std::unique_ptr(new Solver(&options)); - - cout << language::SetLanguage(language::output::LANG_SMTLIB_V2) - << expr::ExprSetDepth(-1); - - // Create the parser - ParserBuilder parserBuilder(solver.get(), input, options); - Parser* parser = parserBuilder.build(); - - // Variables and assertions - vector assertions; - - Command* cmd; - while ((cmd = parser->nextCommand())) { - - AssertCommand* assert = dynamic_cast(cmd); - if (assert) { - Expr normalized = solver->getSmtEngine()->simplify(assert->getExpr()); - cout << "(assert " << normalized << ")" << endl; - delete cmd; - continue; - } - - CheckSatCommand* checksat = dynamic_cast(cmd); - if (checksat) { - delete cmd; - continue; - } - - cout << *cmd << endl; - delete cmd; - } - - cout << "(check-sat)" << endl; - - // Get rid of the parser - delete parser; -} diff --git a/examples/nra-translate/nra-translate-example-input.smt2 b/examples/nra-translate/nra-translate-example-input.smt2 deleted file mode 100644 index 229c46d4a..000000000 --- a/examples/nra-translate/nra-translate-example-input.smt2 +++ /dev/null @@ -1,11 +0,0 @@ -(set-logic QF_NRA) -(set-info :smt-lib-version 2.0) -(set-info :status sat) -(declare-fun x () Real) -(declare-fun y () Real) -(declare-fun n () Real) - -(assert (= (+ x n) 0)) -(assert (= (+ y n) 1)) - -(check-sat) diff --git a/examples/nra-translate/smt2info.cpp b/examples/nra-translate/smt2info.cpp deleted file mode 100644 index a6a210d02..000000000 --- a/examples/nra-translate/smt2info.cpp +++ /dev/null @@ -1,135 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Dejan Jovanovic, Aina Niemetz, Tim King - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * [[ Add one-line brief description here ]] - * - * [[ Add lengthier description here ]] - * \todo document this file - */ - -#include - -#include -#include -#include -#include -#include - -using namespace std; -using namespace cvc5; -using namespace cvc5::parser; -using namespace cvc5::options; - -unsigned compute_degree(ExprManager& exprManager, const Expr& term) { - unsigned n = term.getNumChildren(); - unsigned degree = 0; - - // boolean stuff - if (term.getType() == exprManager.booleanType()) { - for (unsigned i = 0; i < n; ++ i) { - degree = std::max(degree, compute_degree(exprManager, term[i])); - } - return degree; - } - - // terms - if (n == 0) { - if (term.getKind() == kind::CONST_RATIONAL) { - return 0; - } else { - return 1; - } - } else { - unsigned degree = 0; - if (term.getKind() == kind::MULT) { - for (unsigned i = 0; i < n; ++ i) { - degree += std::max(degree, compute_degree(exprManager, term[i])); - } - } else { - for (unsigned i = 0; i < n; ++ i) { - degree = std::max(degree, compute_degree(exprManager, term[i])); - } - } - return degree; - } -} - - -int main(int argc, char* argv[]) -{ - - try { - - // Get the filename - string input(argv[1]); - - // Create the expression manager - Options options; - options.setInputLanguage(language::input::LANG_SMTLIB_V2); - std::unique_ptr solver = - std::unique_ptr(new Solver(&options)); - - // Create the parser - ParserBuilder parserBuilder(solver.get(), input, options); - Parser* parser = parserBuilder.build(); - - // Variables and assertions - vector variables; - vector info_tags; - vector info_data; - vector assertions; - - Command* cmd; - while ((cmd = parser->nextCommand())) { - - SetInfoCommand* setinfo = dynamic_cast(cmd); - if (setinfo) { - info_tags.push_back(setinfo->getFlag()); - info_data.push_back(setinfo->getSExpr().getValue()); - delete cmd; - continue; - } - - DeclareFunctionCommand* declare = dynamic_cast(cmd); - if (declare) { - variables.push_back(declare->getSymbol()); - delete cmd; - continue; - } - - AssertCommand* assert = dynamic_cast(cmd); - if (assert) { - assertions.push_back(assert->getExpr()); - delete cmd; - continue; - } - - delete cmd; - } - - cout << "variables: " << variables.size() << endl; - - unsigned total_degree = 0; - for (unsigned i = 0; i < assertions.size(); ++ i) { - total_degree = - std::max(total_degree, - compute_degree(*solver->getExprManager(), assertions[i])); - } - - cout << "degree: " << total_degree << endl; - - // Get rid of the parser - delete parser; - } catch (Exception& e) { - cerr << e << endl; - } -} diff --git a/examples/nra-translate/smt2todreal.cpp b/examples/nra-translate/smt2todreal.cpp deleted file mode 100644 index 1b3bbdbdb..000000000 --- a/examples/nra-translate/smt2todreal.cpp +++ /dev/null @@ -1,78 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Dejan Jovanovic, Aina Niemetz, Tim King - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * [[ Add one-line brief description here ]] - * - * [[ Add lengthier description here ]] - * \todo document this file - */ - -#include -#include -#include - -#include -#include -#include -#include -#include -#include - -using namespace std; -using namespace cvc5; -using namespace cvc5::parser; -using namespace cvc5::options; - -int main(int argc, char* argv[]) -{ - - // Get the filename - string input(argv[1]); - - // Create the expression manager - Options options; - options.setInputLanguage(language::input::LANG_SMTLIB_V2); - options.setOutputLanguage(language::output::LANG_SMTLIB_V2); - std::unique_ptr solver = - std::unique_ptr(new Solver(&options)); - - cout << expr::ExprDag(0) << expr::ExprSetDepth(-1); - - // Create the parser - ParserBuilder parserBuilder(solver.get(), input, options); - Parser* parser = parserBuilder.build(); - - // Variables and assertions - std::map variables; - vector info_tags; - vector info_data; - vector assertions; - - Command* cmd; - while ((cmd = parser->nextCommand())) { - - DeclareFunctionCommand* declare = dynamic_cast(cmd); - if (declare) { - cout << "[-10000, 10000] " << declare->getSymbol() << ";" << endl; - } - - AssertCommand* assert = dynamic_cast(cmd); - if (assert) { - cout << assert->getExpr() << ";" << endl; - } - - delete cmd; - } - - // Get rid of the parser - delete parser; -} diff --git a/examples/nra-translate/smt2toisat.cpp b/examples/nra-translate/smt2toisat.cpp deleted file mode 100644 index 9dfdfde4f..000000000 --- a/examples/nra-translate/smt2toisat.cpp +++ /dev/null @@ -1,306 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Dejan Jovanovic, Aina Niemetz, Andrew Reynolds - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * [[ Add one-line brief description here ]] - * - * [[ Add lengthier description here ]] - * \todo document this file - */ - -#include - -#include -#include -#include -#include -#include -#include - -using namespace std; -using namespace cvc5; -using namespace cvc5::parser; -using namespace cvc5::options; - -void translate_to_isat( - string input, - const vector& info_tags, - const vector& info_data, - const map& variables, - const vector& assertions); - -int main(int argc, char* argv[]) -{ - - // Get the filename - string input(argv[1]); - - // Create the expression manager - Options options; - options.setInputLanguage(language::input::LANG_SMTLIB_V2); - std::unique_ptr solver = - std::unique_ptr(new Solver(&options)); - - // Create the parser - ParserBuilder parserBuilder(solver.get(), input, options); - Parser* parser = parserBuilder.build(); - - // Variables and assertions - std::map variables; - vector info_tags; - vector info_data; - vector assertions; - - Command* cmd; - while ((cmd = parser->nextCommand())) { - - SetInfoCommand* setinfo = dynamic_cast(cmd); - if (setinfo) { - info_tags.push_back(setinfo->getFlag()); - info_data.push_back(setinfo->getSExpr().getValue()); - delete cmd; - continue; - } - - DeclareFunctionCommand* declare = dynamic_cast(cmd); - if (declare) { - string name = declare->getSymbol(); - Expr var = parser->getVariable(name).getExpr(); - unsigned n = variables.size(); - variables[var] = n; - delete cmd; - continue; - } - - AssertCommand* assert = dynamic_cast(cmd); - if (assert) { - assertions.push_back(solver->getSmtEngine()->simplify(assert->getExpr())); - delete cmd; - continue; - } - - delete cmd; - } - - // Do the translation - translate_to_isat(input, info_tags, info_data, variables, assertions); - - // Get rid of the parser - delete parser; -} - -void translate_to_isat_term(const map& variables, const Expr& term) { - bool first; - - unsigned n = term.getNumChildren(); - - if (n == 0) { - if (term.getKind() == kind::CONST_RATIONAL) { - cout << term.getConst(); - } else { - assert(variables.find(term) != variables.end()); - cout << "x" << variables.find(term)->second; - } - } else { - - switch (term.getKind()) { - case kind::ADD: - cout << "("; - first = true; - for (unsigned i = 0; i < n; ++ i) { - if (!first) { - cout << " + "; - } - first = false; - translate_to_isat_term(variables, term[i]); - } - cout << ")"; - break; - case kind::MULT: - cout << "("; - first = true; - for (unsigned i = 0; i < n; ++ i) { - if (!first) { - cout << " * "; - } - first = false; - translate_to_isat_term(variables, term[i]); - } - cout << ")"; - break; - case kind::MINUS: - cout << "("; - translate_to_isat_term(variables, term[0]); - cout << " - "; - translate_to_isat_term(variables, term[1]); - cout << ")"; - break; - case kind::DIVISION: - assert(false); - break; - case kind::UMINUS: - cout << "(-("; - translate_to_isat_term(variables, term[0]); - cout << "))"; - break; - default: - assert(false); - break; - } - } -} - -void translate_to_isat(const map& variables, const Expr& assertion) { - bool first; - - unsigned n = assertion.getNumChildren(); - - if (n == 0) { - if (assertion.isConst()) { - if (assertion.getConst()) { - cout << "(1 > 0)"; - } else { - cout << "(1 < 0)"; - } - } else { - assert(false); - } - } else { - - std::string op; - bool binary = false; - bool theory = false; - - switch (assertion.getKind()) { - case kind::NOT: - cout << "!"; - translate_to_isat(variables, assertion[0]); - break; - case kind::OR: - first = true; - cout << "("; - for (unsigned i = 0; i < n; ++ i) { - if (!first) { - cout << " or "; - } - first = false; - translate_to_isat(variables, assertion[i]); - } - cout << ")"; - break; - case kind::AND: - first = true; - cout << "("; - for (unsigned i = 0; i < n; ++ i) { - if (!first) { - cout << " and "; - } - first = false; - translate_to_isat(variables, assertion[i]); - } - cout << ")"; - break; - case kind::IMPLIES: - cout << "("; - translate_to_isat(variables, assertion[0]); - cout << " -> "; - translate_to_isat(variables, assertion[1]); - cout << ")"; - break; - case kind::EQUAL: - if( assertion[0].getType().isBoolean() ){ - cout << "("; - translate_to_isat(variables, assertion[0]); - cout << " <-> "; - translate_to_isat(variables, assertion[1]); - cout << ")"; - }else{ - op = "="; - theory = true; - } - break; - case kind::LT: - op = "<"; - theory = true; - break; - case kind::LEQ: - op = "<="; - theory = true; - break; - case kind::GT: - op = ">"; - theory = true; - break; - case kind::GEQ: - op = ">="; - theory = true; - break; - default: - assert(false); - break; - } - - if (binary) { - cout << "("; - translate_to_isat(variables, assertion[0]); - cout << " " << op << " "; - translate_to_isat(variables, assertion[1]); - cout << ")"; - } - - if (theory) { - cout << "("; - translate_to_isat_term(variables, assertion[0]); - cout << " " << op << " "; - translate_to_isat_term(variables, assertion[1]); - cout << ")"; - } - } -} - -void translate_to_isat( - string input, - const vector& info_tags, - const vector& info_data, - const std::map& variables, - const vector& assertions) -{ - bool first; - - // Dump out the information - cout << "-- translated from " << input << endl; - - // Dump the variables - cout << "DECL" << endl; - cout << " -- the variables" << endl; - cout << " float [-1000, 1000]"; - first = true; - for (unsigned i = 0; i < variables.size(); ++ i) { - if (!first) { - cout << ","; - } - cout << " x" << i; - if (first) { - first = false; - } - } - cout << ";" << endl; - - // The assertions - cout << "EXPR" << endl; - cout << " -- the constraints to be solved" << endl; - for (unsigned i = 0; i < assertions.size(); ++ i) { - cout << " "; - translate_to_isat(variables, assertions[i]); - cout << ";" << endl; - } - -} diff --git a/examples/nra-translate/smt2tomathematica.cpp b/examples/nra-translate/smt2tomathematica.cpp deleted file mode 100644 index 5a2a5ce0a..000000000 --- a/examples/nra-translate/smt2tomathematica.cpp +++ /dev/null @@ -1,324 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Dejan Jovanovic, Andrew Reynolds, Aina Niemetz - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * [[ Add one-line brief description here ]] - * - * [[ Add lengthier description here ]] - * \todo document this file - */ - -#include - -#include -#include -#include -#include -#include -#include - -using namespace std; -using namespace cvc5; -using namespace cvc5::parser; - -void translate_to_mathematica( - string input, - const vector& info_tags, - const vector& info_data, - const map& variables, - const vector& assertions); - -int main(int argc, char* argv[]) -{ - - // Get the filename - string input(argv[1]); - - // Create the expression manager - Options options; - options.setInputLanguage(language::input::LANG_SMTLIB_V2); - std::unique_ptr solver = - std::unique_ptr(new Solver(&options)); - - // Create the parser - ParserBuilder parserBuilder(solver.get(), input, options); - Parser* parser = parserBuilder.build(); - - // Variables and assertions - std::map variables; - vector info_tags; - vector info_data; - vector assertions; - - Command* cmd; - while ((cmd = parser->nextCommand())) { - - SetInfoCommand* setinfo = dynamic_cast(cmd); - if (setinfo) { - info_tags.push_back(setinfo->getFlag()); - info_data.push_back(setinfo->getSExpr().getValue()); - delete cmd; - continue; - } - - DeclareFunctionCommand* declare = dynamic_cast(cmd); - if (declare) { - string name = declare->getSymbol(); - Expr var = parser->getVariable(name).getExpr(); - unsigned n = variables.size(); - variables[var] = n; - delete cmd; - continue; - } - - AssertCommand* assert = dynamic_cast(cmd); - if (assert) { - assertions.push_back(assert->getExpr()); - delete cmd; - continue; - } - - delete cmd; - } - - // Do the translation - translate_to_mathematica(input, info_tags, info_data, variables, assertions); - - // Get rid of the parser - delete parser; -} - -void translate_to_mathematica_term(const map& variables, const Expr& term) { - bool first; - - unsigned n = term.getNumChildren(); - - if (n == 0) { - if (term.getKind() == kind::CONST_RATIONAL) { - cout << term.getConst(); - } else { - assert(variables.find(term) != variables.end()); - cout << "x" << variables.find(term)->second; - } - } else { - - switch (term.getKind()) { - case kind::ADD: - cout << "("; - first = true; - for (unsigned i = 0; i < n; ++ i) { - if (!first) { - cout << " + "; - } - first = false; - translate_to_mathematica_term(variables, term[i]); - } - cout << ")"; - break; - case kind::MULT: - cout << "("; - first = true; - for (unsigned i = 0; i < n; ++ i) { - if (!first) { - cout << " * "; - } - first = false; - translate_to_mathematica_term(variables, term[i]); - } - cout << ")"; - break; - case kind::MINUS: - cout << "("; - translate_to_mathematica_term(variables, term[0]); - cout << " - "; - translate_to_mathematica_term(variables, term[1]); - cout << ")"; - break; - case kind::DIVISION: - // we only allow division by constant - assert(term[1].getKind() == kind::CONST_RATIONAL); - cout << "("; - translate_to_mathematica_term(variables, term[0]); - cout << " / "; - translate_to_mathematica_term(variables, term[1]); - cout << ")"; - break; - case kind::UMINUS: - cout << "(-("; - translate_to_mathematica_term(variables, term[0]); - cout << "))"; - break; - default: - assert(false); - break; - } - } -} - -void translate_to_mathematica(const map& variables, const Expr& assertion) { - bool first; - - unsigned n = assertion.getNumChildren(); - - if (n == 0) { - assert(false); - } else { - - std::string op; - bool binary = false; - bool theory = false; - - - switch (assertion.getKind()) { - case kind::NOT: - cout << "!"; - translate_to_mathematica(variables, assertion[0]); - break; - case kind::OR: - first = true; - cout << "("; - for (unsigned i = 0; i < n; ++ i) { - if (!first) { - cout << " || "; - } - first = false; - translate_to_mathematica(variables, assertion[i]); - } - cout << ")"; - break; - case kind::AND: - first = true; - cout << "("; - for (unsigned i = 0; i < n; ++ i) { - if (!first) { - cout << " && "; - } - first = false; - translate_to_mathematica(variables, assertion[i]); - } - cout << ")"; - break; - case kind::IMPLIES: - cout << "Implies["; - translate_to_mathematica(variables, assertion[0]); - cout << ","; - translate_to_mathematica(variables, assertion[1]); - cout << "]"; - break; - case kind::EQUAL: - if( assertion[0].getType().isBoolean() ){ - cout << "Equivalent["; - translate_to_mathematica(variables, assertion[0]); - cout << ","; - translate_to_mathematica(variables, assertion[1]); - cout << "]"; - }else{ - op = "=="; - theory = true; - } - break; - case kind::LT: - op = "<"; - theory = true; - break; - case kind::LEQ: - op = "<="; - theory = true; - break; - case kind::GT: - op = ">"; - theory = true; - break; - case kind::GEQ: - op = ">="; - theory = true; - break; - default: - assert(false); - break; - } - - if (binary) { - cout << "("; - translate_to_mathematica(variables, assertion[0]); - cout << " " << op << " "; - translate_to_mathematica(variables, assertion[1]); - cout << ")"; - } - - if (theory) { - cout << "("; - translate_to_mathematica_term(variables, assertion[0]); - cout << " " << op << " "; - translate_to_mathematica_term(variables, assertion[1]); - cout << ")"; - } - } -} - -void translate_to_mathematica( - string input, - const vector& info_tags, - const vector& info_data, - const std::map& variables, - const vector& assertions) -{ - bool first; - - // Dump out the information - cout << "(* translated from " << input << " "; - - bool dump_tags = false; - if (dump_tags) { - first = true; - for (unsigned i = 0; i < info_tags.size(); ++ i) { - if (!first) { - cout << ", "; - } - first = false; - cout << info_tags[i] << " = " << info_data[i]; - } - } - - cout << "*)" << endl; - - cout << "Resolve["; - - // Formula - cout << "Exists[{"; - first = true; - for (unsigned i = 0; i < variables.size(); ++ i) { - if (!first) { - cout << ","; - } - first = false; - cout << "x" << i; - } - cout << "}, "; - - if (assertions.size() > 1) { - first = true; - for (unsigned i = 0; i < assertions.size(); ++ i) { - if (!first) { - cout << " && "; - } - first = false; - translate_to_mathematica(variables, assertions[i]); - } - } else { - translate_to_mathematica(variables, assertions[0]); - } - cout << "]"; - - - // End resolve - cout << ", Reals]" << endl; -} diff --git a/examples/nra-translate/smt2toqepcad.cpp b/examples/nra-translate/smt2toqepcad.cpp deleted file mode 100644 index a35915723..000000000 --- a/examples/nra-translate/smt2toqepcad.cpp +++ /dev/null @@ -1,353 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Dejan Jovanovic, Tim King, Andrew Reynolds - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * [[ Add one-line brief description here ]] - * - * [[ Add lengthier description here ]] - * \todo document this file - */ - -#include - -#include -#include -#include -#include -#include -#include - -using namespace std; -using namespace cvc5; -using namespace cvc5::parser; - -void translate_to_qepcad( - string input, - const vector& info_tags, - const vector& info_data, - const map& variables, - const vector& assertions); - -int main(int argc, char* argv[]) -{ - std::map vars2id; - - // Get the filename - string input(argv[1]); - - // Create the expression manager - Options options; - options.setInputLanguage(language::input::LANG_SMTLIB_V2); - std::unique_ptr solver = - std::unique_ptr(new Solver(&options)); - - // Create the parser - ParserBuilder parserBuilder(solver.get(), input, options); - Parser* parser = parserBuilder.build(); - - // Variables and assertions - std::map variables; - vector info_tags; - vector info_data; - vector assertions; - - Command* cmd; - while ((cmd = parser->nextCommand())) { - - SetInfoCommand* setinfo = dynamic_cast(cmd); - if (setinfo) { - info_tags.push_back(setinfo->getFlag()); - info_data.push_back(setinfo->getSExpr().getValue()); - delete cmd; - continue; - } - - DeclareFunctionCommand* declare = - dynamic_cast(cmd); - if (declare) { - string name = declare->getSymbol(); - Expr var = parser->getVariable(name).getExpr(); - unsigned n = variables.size(); - variables[var] = n; - delete cmd; - continue; - } - - AssertCommand* assert = dynamic_cast(cmd); - if (assert) { - assertions.push_back(assert->getExpr()); - delete cmd; - continue; - } - - delete cmd; - } - - // Do the translation - translate_to_qepcad(input, info_tags, info_data, variables, assertions); - - // Get rid of the parser - delete parser; -} - -void translate_to_qepcad_term(const std::map& variables, - const Expr& term) -{ - bool first; - - unsigned n = term.getNumChildren(); - - if (n == 0) { - if (term.getKind() == kind::CONST_RATIONAL) { - cout << term.getConst(); - } else { - assert(variables.find(term) != variables.end()); - cout << "x" << variables.find(term)->second; - } - } else { - - switch (term.getKind()) { - case kind::ADD: - cout << "("; - first = true; - for (unsigned i = 0; i < n; ++ i) { - if (!first) { - cout << " + "; - } - first = false; - translate_to_qepcad_term(variables, term[i]); - } - cout << ")"; - break; - case kind::MULT: - cout << "("; - first = true; - for (unsigned i = 0; i < n; ++ i) { - if (!first) { - cout << " "; - } - first = false; - translate_to_qepcad_term(variables, term[i]); - } - cout << ")"; - break; - case kind::MINUS: - cout << "("; - translate_to_qepcad_term(variables, term[0]); - cout << " - "; - translate_to_qepcad_term(variables, term[1]); - cout << ")"; - break; - case kind::UMINUS: - cout << "(-("; - translate_to_qepcad_term(variables, term[0]); - cout << "))"; - break; - case kind::DIVISION: - // we only allow division by constant - assert(term[1].getKind() == kind::CONST_RATIONAL); - cout << "("; - cout << "(1/"; - translate_to_qepcad_term(variables, term[1]); - cout << ") "; - translate_to_qepcad_term(variables, term[0]); - cout << ")"; - break; - default: - assert(false); - break; - } - } -} - -void translate_to_qepcad(const std::map& variables, - const Expr& assertion) -{ - bool first; - - unsigned n = assertion.getNumChildren(); - - if (n == 0) { - assert(false); - } else { - - std::string op; - bool theory = false; - bool binary = false; - - switch (assertion.getKind()) { - case kind::NOT: - cout << "[~"; - translate_to_qepcad(variables, assertion[0]); - cout << "]"; - break; - case kind::OR: - first = true; - cout << "["; - for (unsigned i = 0; i < n; ++ i) { - if (!first) { - cout << " \\/ "; - } - first = false; - translate_to_qepcad(variables, assertion[i]); - } - cout << "]"; - break; - case kind::AND: - first = true; - cout << "["; - for (unsigned i = 0; i < n; ++ i) { - if (!first) { - cout << " /\\ "; - } - first = false; - translate_to_qepcad(variables, assertion[i]); - } - cout << "]"; - break; - case kind::IMPLIES: - op = "==>"; - binary = true; - break; - case kind::EQUAL: - if( assertion[0].getType().isBoolean() ){ - op = "<==>"; - binary = true; - }else{ - op = "="; - theory = true; - } - break; - case kind::LT: - op = "<"; - theory = true; - break; - case kind::LEQ: - op = "<="; - theory = true; - break; - case kind::GT: - op = ">"; - theory = true; - break; - case kind::GEQ: - op = ">="; - theory = true; - break; - default: - assert(false); - break; - } - - if (theory) { - cout << "["; - translate_to_qepcad_term(variables, assertion[0]); - cout << " " << op << " "; - translate_to_qepcad_term(variables, assertion[1]); - cout << "]"; - } - - if (binary) { - cout << "["; - translate_to_qepcad(variables, assertion[0]); - cout << " " << op << " "; - translate_to_qepcad(variables, assertion[1]); - cout << "]"; - } - } -} - -void translate_to_qepcad( - string input, - const vector& info_tags, - const vector& info_data, - const std::map& variables, - const vector& assertions) -{ - bool first; - - // Dump out the information - cout << "[ translated from " << input << " "; - - bool dump_tags = false; - if (dump_tags) { - first = true; - for (unsigned i = 0; i < info_tags.size(); ++ i) { - if (!first) { - cout << ", "; - } - first = false; - cout << info_tags[i] << " = " << info_data[i]; - } - } - - cout << "]" << endl; - - // Declare the variables - cout << "("; - - first = true; - for (unsigned i = 0; i < variables.size(); ++ i) { - if (!first) { - cout << ","; - } - first = false; - cout << "x" << i;; - } - - cout << ")" << endl; - - // Number of free variables - cout << "0" << endl; - - // The quantifiers first - for (unsigned i = 0; i < variables.size(); ++ i) { - cout << "(Ex" << i << ")"; - } - - // Now the formula - cout << "["; - if (assertions.size() > 1) { - first = true; - for (unsigned i = 0; i < assertions.size(); ++ i) { - if (!first) { - cout << " /\\ "; - } - first = false; - translate_to_qepcad(variables, assertions[i]); - } - } else { - translate_to_qepcad(variables, assertions[0]); - } - cout << "]." << endl; - - // Before normalization - cout << "go" << endl; - - // Before projection - if (variables.size() > 3) { - cout << "proj-op (m,m"; - for (unsigned i = 3; i < variables.size(); ++ i) { - cout << ",h"; - } - cout << ")" << endl; - } - cout << "go" << endl; - - // Before choice - cout << "d-stat" << endl; - - // Before solution - cout << "go" << endl; - - // Finish up - cout << "finish" << endl; -} diff --git a/examples/nra-translate/smt2toredlog.cpp b/examples/nra-translate/smt2toredlog.cpp deleted file mode 100644 index 1f7d33902..000000000 --- a/examples/nra-translate/smt2toredlog.cpp +++ /dev/null @@ -1,322 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Dejan Jovanovic, Aina Niemetz, Andrew Reynolds - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * [[ Add one-line brief description here ]] - * - * [[ Add lengthier description here ]] - * \todo document this file - */ - -#include - -#include -#include -#include -#include -#include -#include - -using namespace std; -using namespace cvc5; -using namespace cvc5::parser; -using namespace cvc5::options; - -void translate_to_redlog( - string input, - string command, - const vector& info_tags, - const vector& info_data, - const map& variables, - const vector& assertions); - -int main(int argc, char* argv[]) -{ - - // Get the filename - string input(argv[1]); - // Get the redlog command - string command(argv[2]); - - // Create the expression manager - Options options; - options.setInputLanguage(language::input::LANG_SMTLIB_V2); - std::unique_ptr solver = - std::unique_ptr(new Solver(&options)); - - // Create the parser - ParserBuilder parserBuilder(solver.get(), input, options); - Parser* parser = parserBuilder.build(); - - // Variables and assertions - std::map variables; - vector info_tags; - vector info_data; - vector assertions; - - Command* cmd; - while ((cmd = parser->nextCommand())) { - - SetInfoCommand* setinfo = dynamic_cast(cmd); - if (setinfo) { - info_tags.push_back(setinfo->getFlag()); - info_data.push_back(setinfo->getSExpr().getValue()); - delete cmd; - continue; - } - - DeclareFunctionCommand* declare = dynamic_cast(cmd); - if (declare) { - string name = declare->getSymbol(); - Expr var = parser->getVariable(name).getExpr(); - unsigned n = variables.size(); - variables[var] = n; - delete cmd; - continue; - } - - AssertCommand* assert = dynamic_cast(cmd); - if (assert) { - assertions.push_back(solver->getSmtEngine()->simplify(assert->getExpr())); - delete cmd; - continue; - } - - delete cmd; - } - - // Do the translation - translate_to_redlog(input, command, info_tags, info_data, variables, assertions); - - // Get rid of the parser - delete parser; -} - -void translate_to_redlog_term(const map& variables, const Expr& term) { - bool first; - - unsigned n = term.getNumChildren(); - - if (n == 0) { - if (term.getKind() == kind::CONST_RATIONAL) { - cout << term.getConst(); - } else { - assert(variables.find(term) != variables.end()); - cout << "x" << variables.find(term)->second; - } - } else { - - switch (term.getKind()) { - case kind::ADD: - cout << "("; - first = true; - for (unsigned i = 0; i < n; ++ i) { - if (!first) { - cout << " + "; - } - first = false; - translate_to_redlog_term(variables, term[i]); - } - cout << ")"; - break; - case kind::MULT: - cout << "("; - first = true; - for (unsigned i = 0; i < n; ++ i) { - if (!first) { - cout << " * "; - } - first = false; - translate_to_redlog_term(variables, term[i]); - } - cout << ")"; - break; - case kind::MINUS: - cout << "("; - translate_to_redlog_term(variables, term[0]); - cout << " - "; - translate_to_redlog_term(variables, term[1]); - cout << ")"; - break; - case kind::DIVISION: - cout << "("; - translate_to_redlog_term(variables, term[0]); - cout << " / "; - translate_to_redlog_term(variables, term[1]); - cout << ")"; - break; - case kind::UMINUS: - cout << "(-("; - translate_to_redlog_term(variables, term[0]); - cout << "))"; - break; - default: - assert(false); - break; - } - } -} - -void translate_to_redlog(const map& variables, const Expr& assertion) { - bool first; - - unsigned n = assertion.getNumChildren(); - - if (n == 0) { - if (assertion.isConst()) { - if (assertion.getConst()) { - cout << "(1 > 0)"; - } else { - cout << "(1 < 0)"; - } - } else { - assert(false); - } - } else { - - std::string op; - bool binary = false; - bool theory = false; - - switch (assertion.getKind()) { - case kind::NOT: - cout << "(not "; - translate_to_redlog(variables, assertion[0]); - cout << ")"; - break; - case kind::OR: - first = true; - cout << "("; - for (unsigned i = 0; i < n; ++ i) { - if (!first) { - cout << " or "; - } - first = false; - translate_to_redlog(variables, assertion[i]); - } - cout << ")"; - break; - case kind::AND: - first = true; - cout << "("; - for (unsigned i = 0; i < n; ++ i) { - if (!first) { - cout << " and "; - } - first = false; - translate_to_redlog(variables, assertion[i]); - } - cout << ")"; - break; - case kind::IMPLIES: - cout << "("; - translate_to_redlog(variables, assertion[0]); - cout << " impl "; - translate_to_redlog(variables, assertion[1]); - cout << ")"; - break; - case kind::EQUAL: - if( assertion[0].getType().isBoolean() ){ - cout << "("; - translate_to_redlog(variables, assertion[0]); - cout << " equiv "; - translate_to_redlog(variables, assertion[1]); - cout << ")"; - }else{ - op = "="; - theory = true; - } - break; - case kind::LT: - op = "<"; - theory = true; - break; - case kind::LEQ: - op = "<="; - theory = true; - break; - case kind::GT: - op = ">"; - theory = true; - break; - case kind::GEQ: - op = ">="; - theory = true; - break; - default: - assert(false); - break; - } - - if (binary) { - cout << "("; - translate_to_redlog(variables, assertion[0]); - cout << " " << op << " "; - translate_to_redlog(variables, assertion[1]); - cout << ")"; - } - - if (theory) { - cout << "("; - translate_to_redlog_term(variables, assertion[0]); - cout << " " << op << " "; - translate_to_redlog_term(variables, assertion[1]); - cout << ")"; - } - } -} - -void translate_to_redlog( - string input, - string command, - const vector& info_tags, - const vector& info_data, - const std::map& variables, - const vector& assertions) -{ - bool first; - - // Dump out the information - cout << "load redlog;" << endl; - cout << "rlset ofsf;" << endl; - - // Dump the variables - - cout << "phi := ex({"; - first = true; - for (unsigned i = 0; i < variables.size(); ++ i) { - if (!first) { - cout << ","; - } - cout << " x" << i; - if (first) { - first = false; - } - } - cout << "},"; - - // The assertions - first = true; - for (unsigned i = 0; i < assertions.size(); ++ i) { - if (first == false) { - cout << " and "; - } - first = false; - translate_to_redlog(variables, assertions[i]); - - } - cout << ");" << endl; - - cout << "result := " << command << " phi;" << endl; - cout << "result;" << endl; - cout << "quit;" << endl; - -} diff --git a/examples/sets-translate/CMakeLists.txt b/examples/sets-translate/CMakeLists.txt deleted file mode 100644 index d1a8650ce..000000000 --- a/examples/sets-translate/CMakeLists.txt +++ /dev/null @@ -1,28 +0,0 @@ -############################################################################### -# Top contributors (to current version): -# Aina Niemetz, Mathias Preiner -# -# This file is part of the cvc5 project. -# -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS -# in the top-level source directory and their institutional affiliations. -# All rights reserved. See the file COPYING in the top-level source -# directory for licensing information. -# ############################################################################# -# -# The build system configuration. -## - -if(Boost_FOUND) - cvc5_add_example(sets2arrays - "sets_translate.cpp" "sets-translate" - # argument to binary (for testing) - ${CMAKE_CURRENT_SOURCE_DIR}/sets-translate-example-input.smt2) - - cvc5_add_example(sets2axioms - "sets_translate.cpp" "sets-translate" - # argument to binary (for testing) - ${CMAKE_CURRENT_SOURCE_DIR}/sets-translate-example-input.smt2) - target_compile_definitions(sets2axioms PRIVATE -DENABLE_AXIOMS) -endif() - diff --git a/examples/sets-translate/sets-translate-example-input.smt2 b/examples/sets-translate/sets-translate-example-input.smt2 deleted file mode 100644 index 1dfb50803..000000000 --- a/examples/sets-translate/sets-translate-example-input.smt2 +++ /dev/null @@ -1,20 +0,0 @@ -(set-logic ALL) -(declare-sort Atom 0) - -(declare-fun k (Atom Atom) (Set Atom)) - -(declare-fun t0 () Atom) -(declare-fun t1 () Atom) -(declare-fun t2 () Atom) -(declare-fun v () Atom) -(declare-fun b2 () Atom) - -(assert (forall ((b Atom)) (or -(set.member v (k t0 b)) -(set.member v (k t1 b)) -) )) - -(assert (not (set.member v (k t2 b2)))) - -(check-sat) - diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp deleted file mode 100644 index 8eac076d2..000000000 --- a/examples/sets-translate/sets_translate.cpp +++ /dev/null @@ -1,386 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Kshitij Bansal, Andres Noetzli, Tim King - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * [[ Add one-line brief description here ]] - * - * [[ Add lengthier description here ]] - * \todo document this file - */ - -#include -#include - -#include // include Boost, a C++ library -#include -#include -#include -#include -#include -#include - -using namespace std; -using namespace cvc5; -using namespace cvc5::parser; -using namespace cvc5::options; - -bool nonsense(char c) { return !isalnum(c); } - -#ifdef ENABLE_AXIOMS -const bool enableAxioms = true; -#else -const bool enableAxioms = false; -#endif - -string setaxioms[] = { - "(declare-fun memberHOLDA (HOLDB (Set HOLDB)) Bool)", - "", - "(declare-fun unionHOLDA ((Set HOLDB) (Set HOLDB)) (Set HOLDB))", - "(assert (forall ((?X (Set HOLDB)) (?Y (Set HOLDB)) (?x HOLDB))", - " (= (memberHOLDA ?x (unionHOLDA ?X ?Y))", - " (or (memberHOLDA ?x ?X) (memberHOLDA ?x ?Y))", - " ) ) )", - "", - "", - "(declare-fun intersectionHOLDA ((Set HOLDB) (Set HOLDB)) (Set HOLDB))", - "(assert (forall ((?X (Set HOLDB)) (?Y (Set HOLDB)) (?x HOLDB))", - " (= (memberHOLDA ?x (intersectionHOLDA ?X ?Y))", - " (and (memberHOLDA ?x ?X) (memberHOLDA ?x ?Y))", - " ) ) )", - "", - "(declare-fun setminusHOLDA ((Set HOLDB) (Set HOLDB)) (Set HOLDB))", - "(assert (forall ((?X (Set HOLDB)) (?Y (Set HOLDB)) (?x HOLDB))", - " (= (memberHOLDA ?x (setminusHOLDA ?X ?Y))", - " (and (memberHOLDA ?x ?X) (not (memberHOLDA ?x ?Y)))", - " ) ) )", - "", - "(declare-fun singletonHOLDA (HOLDB) (Set HOLDB))", - "(assert (forall ((?x HOLDB) (?y HOLDB))", - " (= (memberHOLDA ?x (singletonHOLDA ?y))", - " (= ?x ?y)", - " ) ) )", - "", - "(declare-fun emptysetHOLDA () (Set HOLDB))", - "(assert (forall ((?x HOLDB)) (not (memberHOLDA ?x emptysetHOLDA)) ) )", - "", - "(define-fun subsetHOLDA ((X (Set HOLDB)) (Y (Set HOLDB))) Bool (= (unionHOLDA X Y) Y))", - "" -}; - -class Mapper { - set< Type > setTypes; - map< Type, Type > mapTypes; - map< pair, Expr > setoperators; - unordered_map< Expr, Expr, ExprHashFunction > substitutions; - ostringstream sout; - ExprManager* em; - int depth; - - Expr add(SetType t, Expr e) { - - if(setTypes.find(t) == setTypes.end() ) { - // mark as processed - setTypes.insert(t); - - Type elementType = t.getElementType(); - ostringstream oss_type; - oss_type << language::SetLanguage(language::output::LANG_SMTLIB_V2) - << elementType; - string elementTypeAsString = oss_type.str(); - elementTypeAsString.erase( - remove_if(elementTypeAsString.begin(), elementTypeAsString.end(), nonsense), - elementTypeAsString.end()); - - // define-sort - ostringstream oss_name; - oss_name << language::SetLanguage(language::output::LANG_SMTLIB_V2) - << "(Set " << elementType << ")"; - string name = oss_name.str(); - Type newt = em->mkArrayType(t.getElementType(), em->booleanType()); - mapTypes[t] = newt; - - // diffent types - vector t_t; - t_t.push_back(t); - t_t.push_back(t); - vector elet_t; - elet_t.push_back(elementType); - elet_t.push_back(t); - - if(!enableAxioms) - sout << "(define-fun emptyset" << elementTypeAsString << " " - << " ()" - << " " << name - << " ( (as const " << name << ") false ) )" << endl; - setoperators[make_pair(t, kind::SET_EMPTY)] = - em->mkVar(std::string("emptyset") + elementTypeAsString, t); - - if(!enableAxioms) - sout << "(define-fun singleton" << elementTypeAsString << " " - << " ( (x " << elementType << ") )" - << " " << name << "" - << " (store emptyset" << elementTypeAsString << " x true) )" << endl; - setoperators[make_pair(t, kind::SET_SINGLETON)] = - em->mkVar(std::string("singleton") + elementTypeAsString, - em->mkFunctionType(elementType, t)); - - if(!enableAxioms) - sout << "(define-fun union" << elementTypeAsString << " " - << " ( (s1 " << name << ") (s2 " << name << ") )" - << " " << name << "" - << " ((_ map or) s1 s2))" << endl; - setoperators[make_pair(t, kind::SET_UNION)] = - em->mkVar(std::string("union") + elementTypeAsString, - em->mkFunctionType(t_t, t)); - - if(!enableAxioms) - sout << "(define-fun intersection" << elementTypeAsString << "" - << " ( (s1 " << name << ") (s2 " << name << ") )" - << " " << name << "" - << " ((_ map and) s1 s2))" << endl; - setoperators[make_pair(t, kind::SET_INTER)] = - em->mkVar(std::string("intersection") + elementTypeAsString, - em->mkFunctionType(t_t, t)); - - if(!enableAxioms) - sout << "(define-fun setminus" << elementTypeAsString << " " - << " ( (s1 " << name << ") (s2 " << name << ") )" - << " " << name << "" - << " (intersection" << elementTypeAsString << " s1 ((_ map not) s2)))" << endl; - setoperators[make_pair(t, kind::SET_MINUS)] = - em->mkVar(std::string("setminus") + elementTypeAsString, - em->mkFunctionType(t_t, t)); - - if(!enableAxioms) - sout << "(define-fun member" << elementTypeAsString << " " - << " ( (x " << elementType << ")" << " (s " << name << "))" - << " Bool" - << " (select s x) )" << endl; - setoperators[make_pair(t, kind::SET_MEMBER)] = - em->mkVar(std::string("member") + elementTypeAsString, - em->mkPredicateType(elet_t)); - - if(!enableAxioms) - sout << "(define-fun subset" << elementTypeAsString << " " - << " ( (s1 " << name << ") (s2 " << name << ") )" - << " Bool" - <<" (= emptyset" << elementTypeAsString << " (setminus" << elementTypeAsString << " s1 s2)) )" << endl; - setoperators[make_pair(t, kind::SET_SUBSET)] = - em->mkVar(std::string("subset") + elementTypeAsString, - em->mkPredicateType(t_t)); - - if(enableAxioms) { - int N = sizeof(setaxioms) / sizeof(setaxioms[0]); - for(int i = 0; i < N; ++i) { - string s = setaxioms[i]; - ostringstream oss; - oss << language::SetLanguage(language::output::LANG_SMTLIB_V2) << elementType; - boost::replace_all(s, "HOLDA", elementTypeAsString); - boost::replace_all(s, "HOLDB", oss.str()); - if( s == "" ) continue; - sout << s << endl; - } - } - - } - Expr ret; - if (e.getKind() == kind::SET_EMPTY) - { - ret = setoperators[ make_pair(t, e.getKind()) ]; - } - else - { - vector children = e.getChildren(); - children.insert(children.begin(), setoperators[ make_pair(t, e.getKind()) ]); - ret = em->mkExpr(kind::APPLY_UF, children); - } - // cout << "returning " << ret << endl; - return ret; - } - -public: - Mapper(ExprManager* e) : em(e),depth(0) { - sout << language::SetLanguage(language::output::LANG_SMTLIB_V2); - } - - void defineSetSort() { - if(setTypes.empty()) { - cout << "(define-sort Set (X) (Array X Bool) )" << endl; - } - } - - - Expr collectSortsExpr(Expr e) - { - if(substitutions.find(e) != substitutions.end()) { - return substitutions[e]; - } - ++depth; - Expr old_e = e; - for(unsigned i = 0; i < e.getNumChildren(); ++i) { - collectSortsExpr(e[i]); - } - e = e.substitute(substitutions); - // cout << "[debug] " << e << " " << e.getKind() << " " << theory::kindToTheoryId(e.getKind()) << endl; - if(theory::kindToTheoryId(e.getKind()) == theory::THEORY_SETS) { - SetType t = SetType(e.getType().isBoolean() ? e[1].getType() : e.getType()); - substitutions[e] = add(t, e); - e = e.substitute(substitutions); - } - substitutions[old_e] = e; - // cout << ";"; for(int i = 0; i < depth; ++i) cout << " "; cout << old_e << " => " << e << endl; - --depth; - return e; - } - - void dump() { - cout << sout.str(); - } -}; - - -int main(int argc, char* argv[]) -{ - - try { - - // Get the filename - string input; - if(argc > 1){ - input = string(argv[1]); - } else { - input = ""; - } - - // Create the expression manager - Options options; - options.setInputLanguage(language::input::LANG_SMTLIB_V2); - cout << language::SetLanguage(language::output::LANG_SMTLIB_V2); - // cout << Expr::dag(0); - std::unique_ptr solver = - std::unique_ptr(new Solver(&options)); - - Mapper m(solver->getExprManager()); - - // Create the parser - ParserBuilder parserBuilder(solver.get(), input, options); - if(input == "") parserBuilder.withStreamInput(cin); - std::unique_ptr parser; - parser.reset(parserBuilder.build()); - - // Variables and assertions - vector variables; - vector info_tags; - vector info_data; - vector assertions; - - Command* cmd = NULL; - CommandSequence commandsSequence; - bool logicisset = false; - - while ((cmd = parser->nextCommand())) { - - // till logic is set, don't do any modifications - if(!parser->logicIsSet()) { - cout << (*cmd) << endl; - delete cmd; - continue; - } - - // transform set-logic command, if there is one - SetBenchmarkLogicCommand* setlogic = dynamic_cast(cmd); - if(setlogic) { - LogicInfo logicinfo(setlogic->getLogic()); - if(!logicinfo.isTheoryEnabled(theory::THEORY_SETS)) { - cerr << "Sets theory not enabled. Stopping translation." << endl; - return 0; - } - logicinfo = logicinfo.getUnlockedCopy(); - if(enableAxioms) { - logicinfo.enableQuantifiers(); - logicinfo.lock(); - if(!logicinfo.hasEverything()) { - (logicinfo = logicinfo.getUnlockedCopy()).disableTheory(theory::THEORY_SETS); - logicinfo.lock(); - cout << SetBenchmarkLogicCommand(logicinfo.getLogicString()) << endl; - } - } else { - logicinfo.enableTheory(theory::THEORY_ARRAYS); - // we print logic string only for Quantifiers, for Z3 stuff - // we don't set the logic - } - - delete cmd; - continue; - } - - // if we reach here, logic is set by now, so can define our sort - if( !logicisset ) { - logicisset = true; - m.defineSetSort(); - } - - // declare/define-sort commands are printed immediately - DeclareTypeCommand* declaresort = dynamic_cast(cmd); - DefineTypeCommand* definesort = dynamic_cast(cmd); - if(declaresort || definesort) { - cout << *cmd << endl; - delete cmd; - continue; - } - - // other commands are queued up, while replacing with new function symbols - AssertCommand* assert = dynamic_cast(cmd); - DeclareFunctionCommand* declarefun = dynamic_cast(cmd); - DefineFunctionCommand* definefun = dynamic_cast(cmd); - - Command* new_cmd = NULL; - if (assert) - { - Expr newexpr = m.collectSortsExpr(assert->getExpr()); - new_cmd = new AssertCommand(newexpr); - } - else if (declarefun) - { - Expr newfunc = m.collectSortsExpr(declarefun->getFunction()); - new_cmd = new DeclareFunctionCommand( - declarefun->getSymbol(), newfunc, declarefun->getType()); - } - else if (definefun) - { - Expr newfunc = m.collectSortsExpr(definefun->getFunction()); - Expr newformula = m.collectSortsExpr(definefun->getFormula()); - new_cmd = new DefineFunctionCommand(definefun->getSymbol(), - newfunc, - definefun->getFormals(), - newformula, - false); - } - - if(new_cmd == NULL) { - commandsSequence.addCommand(cmd); - } else { - commandsSequence.addCommand(new_cmd); - delete cmd; - } - - } - - m.dump(); - cout << commandsSequence; - - - // Get rid of the parser - //delete parser; - } catch (Exception& e) { - cerr << e << endl; - } -} diff --git a/examples/translator-example-input.smt2 b/examples/translator-example-input.smt2 deleted file mode 100644 index be230b113..000000000 --- a/examples/translator-example-input.smt2 +++ /dev/null @@ -1,20 +0,0 @@ -(set-logic ALL) -(declare-sort Atom 0) - -(declare-fun k (Atom Atom) (Set Atom)) - -(declare-fun t0 () Atom) -(declare-fun t1 () Atom) -(declare-fun t2 () Atom) -(declare-fun v () Atom) -(declare-fun b2 () Atom) - -(assert (forall ((b Atom)) (or -(member v (k t0 b)) -(member v (k t1 b)) -) )) - -(assert (not (member v (k t2 b2)))) - -(check-sat) - diff --git a/examples/translator.cpp b/examples/translator.cpp deleted file mode 100644 index 6a7c8a542..000000000 --- a/examples/translator.cpp +++ /dev/null @@ -1,283 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Morgan Deters, Aina Niemetz, Tim King - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * CVC4 translator - * - * The CVC4 translator executable. This program translates from one of - * CVC4's input languages to one of its output languages. - */ - -#include -#include -#include -#include - -#include -#include -#include -#include -#include - -using namespace std; -using namespace cvc5; -using namespace cvc5::language; -using namespace cvc5::parser; - -enum { - INPUT_LANG = 'L', - OUTPUT_LANG = 'O', - OUTPUT_FILE = 'o', - HELP = 'h', - DEFAULT_DAG_THRESH, - EXPAND_DEFINITIONS, - COMBINE_ASSERTIONS, -};/* enum */ - -const struct option longopts[] = { - { "output-lang", required_argument, NULL, OUTPUT_LANG }, - { "output-language", required_argument, NULL, OUTPUT_LANG }, - { "expand-definitions", no_argument, NULL, EXPAND_DEFINITIONS }, - { "combine-assertions", no_argument, NULL, COMBINE_ASSERTIONS }, - { "dag-thresh", required_argument, NULL, DEFAULT_DAG_THRESH }, - { "lang", required_argument, NULL, INPUT_LANG }, - { "language", required_argument, NULL, INPUT_LANG }, - { "out", required_argument, NULL, OUTPUT_FILE }, - { "help", no_argument, NULL, HELP }, - { NULL, no_argument, NULL, 0 }, -};/* longopts */ - -static void showHelp() { - cerr << "cvc4-translator translation tool" << endl - << " --output-language | -O set output language (default smt2)" << endl - << " --input-language | -L set input language (default auto)" << endl - << " --out | -o set output file (- for stdout)" << endl - << " --dag-thresh=N set DAG threshold" << endl - << " --expand-definitions expand define-funs" << endl - << " --combine-assertions combine all assertions into one" << endl - << " --help | -h this help" << endl - << "Options and input filenames can be intermixed, and order is important." << endl - << "For instance, \"-O smt2 x -O cvc4 y\" reads file x in smt2 format and" - << "file y in cvc4 format and writes all output to stdout." << endl - << "Some canonicalization may occur." << endl - << "Comments and formatting are not preserved." << endl; -} - -static void readFile(const char* filename, InputLanguage fromLang, OutputLanguage toLang, bool expand_definitions, bool combine_assertions, ostream* out) { - if(fromLang == input::LANG_AUTO) { - unsigned len = strlen(filename); - if(len >= 5 && !strcmp(".smt2", filename + len - 5)) { - fromLang = language::input::LANG_SMTLIB_V2; - } else if((len >= 2 && !strcmp(".p", filename + len - 2)) || - (len >= 5 && !strcmp(".tptp", filename + len - 5))) { - fromLang = language::input::LANG_TPTP; - } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) ) || - ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) { - fromLang = language::input::LANG_CVC4; - } else { - throw Exception("cannot determine input language to use for `" + string(filename) + "'"); - } - } - - if(toLang == output::LANG_AUTO) { - toLang = toOutputLanguage(fromLang); - } - - *out << language::SetLanguage(toLang); - - Options opts; - opts.setInputLanguage(fromLang); - ExprManager exprMgr(opts); - std::unique_ptr solver = std::unique_ptr(new Solver(&opts)); - ParserBuilder parserBuilder(solver.get(), filename, opts); - if(!strcmp(filename, "-")) { - parserBuilder.withFilename(""); - parserBuilder.withLineBufferedStreamInput(cin); - } - Parser *parser = parserBuilder.build(); - // we only use the SmtEngine to do definition expansion for us - SmtEngine *smt = expand_definitions ? new SmtEngine(&exprMgr) : NULL; - // store up the assertions into one big conjunction - std::vector assertions; - while(Command* cmd = parser->nextCommand()) { - if(expand_definitions && dynamic_cast(cmd) != NULL) { - // tell the SmtEngine about the definition, but don't print it - cmd->invoke(smt); - } else { - // have to switch on the command and expand definitions inside it - if(expand_definitions && dynamic_cast(cmd) != NULL) { - Expr e = static_cast(cmd)->getExpr(); - delete cmd; - cmd = new AssertCommand(smt->expandDefinitions(e)); - } else if(expand_definitions && dynamic_cast(cmd) != NULL) { - Expr e = static_cast(cmd)->getExpr(); - delete cmd; - cmd = new QueryCommand(smt->expandDefinitions(e)); - } else if(expand_definitions && dynamic_cast(cmd) != NULL) { - Expr e = static_cast(cmd)->getExpr(); - delete cmd; - cmd = new CheckSatCommand(smt->expandDefinitions(e)); - } else if(expand_definitions && dynamic_cast(cmd) != NULL) { - Expr e = static_cast(cmd)->getTerm(); - delete cmd; - cmd = new SimplifyCommand(smt->expandDefinitions(e)); - } else if(expand_definitions && dynamic_cast(cmd) != NULL) { - Expr e = static_cast(cmd)->getTerm(); - delete cmd; - cmd = new ExpandDefinitionsCommand(smt->expandDefinitions(e)); - } else if(expand_definitions && dynamic_cast(cmd) != NULL) { - vector terms = static_cast(cmd)->getTerms(); - delete cmd; - for(size_t i = 0; i < terms.size(); ++i) { - terms[i] = smt->expandDefinitions(terms[i]); - } - cmd = new GetValueCommand(terms); - } - - if(combine_assertions && dynamic_cast(cmd) != NULL) { - // store up the assertion, don't print it yet - assertions.push_back(static_cast(cmd)->getExpr()); - } else { - if(combine_assertions && - ( dynamic_cast(cmd) != NULL || - dynamic_cast(cmd) != NULL || - dynamic_cast(cmd) != NULL || - dynamic_cast(cmd) != NULL || - dynamic_cast(cmd) != NULL || - dynamic_cast(cmd) != NULL )) { - // combine all the stored assertions and print them at this point - if(!assertions.empty()) { - if(assertions.size() > 1) { - *out << AssertCommand(exprMgr.mkExpr(kind::AND, assertions)) << endl; - } else { - *out << AssertCommand(assertions[0]) << endl; - } - assertions.clear(); - } - } - - // now print the cmd we just parsed - *out << cmd << endl; - } - } - if(dynamic_cast(cmd) != NULL) { - delete cmd; - break; - } - delete cmd; - } - if(!assertions.empty()) { - if(assertions.size() > 1) { - *out << AssertCommand(exprMgr.mkExpr(kind::AND, assertions)) << endl; - } else { - *out << AssertCommand(assertions[0]) << endl; - } - assertions.clear(); - } - *out << flush; - delete smt; - delete parser; -} - -/** - * Translate from an input language to an output language. - */ -int main(int argc, char* argv[]) { - ostream* out = &cout; - InputLanguage fromLang = input::LANG_AUTO; - OutputLanguage toLang = output::LANG_SMTLIB_V2; - size_t files = 0; - int dag_thresh = 1; - bool expand_definitions = false; - bool combine_assertions = false; - - try { - int c; - while((c = getopt_long(argc, argv, "-L:O:o:h", longopts, NULL)) != -1) { - switch(c) { - case 1: - ++files; - *out << expr::ExprDag(dag_thresh); - readFile(optarg, (!strcmp(optarg, "-") && fromLang == input::LANG_AUTO) ? input::LANG_CVC4 : fromLang, toLang, expand_definitions, combine_assertions, out); - break; - case INPUT_LANG: - if(!strcmp(optarg, "help")) { - Options::printLanguageHelp(cerr); - exit(1); - } - fromLang = toInputLanguage(optarg); - break; - case OUTPUT_LANG: - if(!strcmp(optarg, "help")) { - Options::printLanguageHelp(cerr); - exit(1); - } - toLang = toOutputLanguage(optarg); - break; - case OUTPUT_FILE: - out->flush(); - if(out != &cout) { - ((ofstream*)out)->close(); - delete out; - } - if(strcmp(optarg, "-")) { - out = new ofstream(optarg); - } else { - out = &cout; - } - break; - case DEFAULT_DAG_THRESH: { - if(!isdigit(*optarg)) { - cerr << "error: --dag-thresh requires non-negative argument: `" - << optarg << "' invalid." << endl; - exit(1); - } - char* end; - unsigned long ul = strtoul(optarg, &end, 10); - if(errno != 0 || *end != '\0') { - cerr << "error: --dag-thresh argument malformed: `" - << optarg << "'." << endl; - exit(1); - } - dag_thresh = ul > INT_MAX ? INT_MAX : int(ul); - } - break; - case EXPAND_DEFINITIONS: - expand_definitions = true; - break; - case COMBINE_ASSERTIONS: - combine_assertions = true; - break; - case 'h': - showHelp(); - exit(0); - case '?': - showHelp(); - exit(1); - default: - cerr << "internal error. translator failed (" - << char(c) << "," << c << ")." << endl; - exit(1); - } - } - - if(files == 0) { - *out << expr::ExprDag(dag_thresh); - readFile("-", fromLang == input::LANG_AUTO ? input::LANG_CVC4 : fromLang, toLang, expand_definitions, combine_assertions, out); - exit(0); - } - } catch(Exception& e) { - cerr << e << endl; - exit(1); - } - - return 0; -}