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)
+++ /dev/null
-###############################################################################
-# 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()
+++ /dev/null
-/******************************************************************************
- * 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 <cvc5/cvc5.h>
-#include <cvc4/expr/expr_iomanip.h>
-#include <cvc4/options/set_language.h>
-
-#include <cassert>
-#include <iostream>
-#include <map>
-#include <string>
-#include <typeinfo>
-#include <vector>
-
-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> solver =
- std::unique_ptr<Solver>(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<Expr> assertions;
-
- Command* cmd;
- while ((cmd = parser->nextCommand())) {
-
- AssertCommand* assert = dynamic_cast<AssertCommand*>(cmd);
- if (assert) {
- Expr normalized = solver->getSmtEngine()->simplify(assert->getExpr());
- cout << "(assert " << normalized << ")" << endl;
- delete cmd;
- continue;
- }
-
- CheckSatCommand* checksat = dynamic_cast<CheckSatCommand*>(cmd);
- if (checksat) {
- delete cmd;
- continue;
- }
-
- cout << *cmd << endl;
- delete cmd;
- }
-
- cout << "(check-sat)" << endl;
-
- // Get rid of the parser
- delete parser;
-}
+++ /dev/null
-(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)
+++ /dev/null
-/******************************************************************************
- * 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 <cvc5/cvc5.h>
-
-#include <cassert>
-#include <iostream>
-#include <string>
-#include <typeinfo>
-#include <vector>
-
-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> solver =
- std::unique_ptr<Solver>(new Solver(&options));
-
- // Create the parser
- ParserBuilder parserBuilder(solver.get(), input, options);
- Parser* parser = parserBuilder.build();
-
- // Variables and assertions
- vector<string> variables;
- vector<string> info_tags;
- vector<string> info_data;
- vector<Expr> assertions;
-
- Command* cmd;
- while ((cmd = parser->nextCommand())) {
-
- SetInfoCommand* setinfo = dynamic_cast<SetInfoCommand*>(cmd);
- if (setinfo) {
- info_tags.push_back(setinfo->getFlag());
- info_data.push_back(setinfo->getSExpr().getValue());
- delete cmd;
- continue;
- }
-
- DeclareFunctionCommand* declare = dynamic_cast<DeclareFunctionCommand*>(cmd);
- if (declare) {
- variables.push_back(declare->getSymbol());
- delete cmd;
- continue;
- }
-
- AssertCommand* assert = dynamic_cast<AssertCommand*>(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;
- }
-}
+++ /dev/null
-/******************************************************************************
- * 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 <cvc5/cvc5.h>
-#include <cvc4/expr/expr_iomanip.h>
-#include <cvc4/options/set_language.h>
-
-#include <cassert>
-#include <iostream>
-#include <map>
-#include <string>
-#include <typeinfo>
-#include <vector>
-
-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> solver =
- std::unique_ptr<Solver>(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<Expr, unsigned> variables;
- vector<string> info_tags;
- vector<string> info_data;
- vector<Expr> assertions;
-
- Command* cmd;
- while ((cmd = parser->nextCommand())) {
-
- DeclareFunctionCommand* declare = dynamic_cast<DeclareFunctionCommand*>(cmd);
- if (declare) {
- cout << "[-10000, 10000] " << declare->getSymbol() << ";" << endl;
- }
-
- AssertCommand* assert = dynamic_cast<AssertCommand*>(cmd);
- if (assert) {
- cout << assert->getExpr() << ";" << endl;
- }
-
- delete cmd;
- }
-
- // Get rid of the parser
- delete parser;
-}
+++ /dev/null
-/******************************************************************************
- * 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 <cvc5/cvc5.h>
-
-#include <cassert>
-#include <iostream>
-#include <map>
-#include <string>
-#include <typeinfo>
-#include <vector>
-
-using namespace std;
-using namespace cvc5;
-using namespace cvc5::parser;
-using namespace cvc5::options;
-
-void translate_to_isat(
- string input,
- const vector<string>& info_tags,
- const vector<string>& info_data,
- const map<Expr, unsigned>& variables,
- const vector<Expr>& 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> solver =
- std::unique_ptr<Solver>(new Solver(&options));
-
- // Create the parser
- ParserBuilder parserBuilder(solver.get(), input, options);
- Parser* parser = parserBuilder.build();
-
- // Variables and assertions
- std::map<Expr, unsigned> variables;
- vector<string> info_tags;
- vector<string> info_data;
- vector<Expr> assertions;
-
- Command* cmd;
- while ((cmd = parser->nextCommand())) {
-
- SetInfoCommand* setinfo = dynamic_cast<SetInfoCommand*>(cmd);
- if (setinfo) {
- info_tags.push_back(setinfo->getFlag());
- info_data.push_back(setinfo->getSExpr().getValue());
- delete cmd;
- continue;
- }
-
- DeclareFunctionCommand* declare = dynamic_cast<DeclareFunctionCommand*>(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<AssertCommand*>(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<Expr, unsigned>& variables, const Expr& term) {
- bool first;
-
- unsigned n = term.getNumChildren();
-
- if (n == 0) {
- if (term.getKind() == kind::CONST_RATIONAL) {
- cout << term.getConst<Rational>();
- } 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<Expr, unsigned>& variables, const Expr& assertion) {
- bool first;
-
- unsigned n = assertion.getNumChildren();
-
- if (n == 0) {
- if (assertion.isConst()) {
- if (assertion.getConst<bool>()) {
- 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<string>& info_tags,
- const vector<string>& info_data,
- const std::map<Expr, unsigned>& variables,
- const vector<Expr>& 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;
- }
-
-}
+++ /dev/null
-/******************************************************************************
- * 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 <cvc5/cvc5.h>
-
-#include <cassert>
-#include <iostream>
-#include <map>
-#include <string>
-#include <typeinfo>
-#include <vector>
-
-using namespace std;
-using namespace cvc5;
-using namespace cvc5::parser;
-
-void translate_to_mathematica(
- string input,
- const vector<string>& info_tags,
- const vector<string>& info_data,
- const map<Expr, unsigned>& variables,
- const vector<Expr>& 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> solver =
- std::unique_ptr<Solver>(new Solver(&options));
-
- // Create the parser
- ParserBuilder parserBuilder(solver.get(), input, options);
- Parser* parser = parserBuilder.build();
-
- // Variables and assertions
- std::map<Expr, unsigned> variables;
- vector<string> info_tags;
- vector<string> info_data;
- vector<Expr> assertions;
-
- Command* cmd;
- while ((cmd = parser->nextCommand())) {
-
- SetInfoCommand* setinfo = dynamic_cast<SetInfoCommand*>(cmd);
- if (setinfo) {
- info_tags.push_back(setinfo->getFlag());
- info_data.push_back(setinfo->getSExpr().getValue());
- delete cmd;
- continue;
- }
-
- DeclareFunctionCommand* declare = dynamic_cast<DeclareFunctionCommand*>(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<AssertCommand*>(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<Expr, unsigned>& variables, const Expr& term) {
- bool first;
-
- unsigned n = term.getNumChildren();
-
- if (n == 0) {
- if (term.getKind() == kind::CONST_RATIONAL) {
- cout << term.getConst<Rational>();
- } 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<Expr, unsigned>& 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<string>& info_tags,
- const vector<string>& info_data,
- const std::map<Expr, unsigned>& variables,
- const vector<Expr>& 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;
-}
+++ /dev/null
-/******************************************************************************
- * 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 <cvc5/cvc5.h>
-
-#include <cassert>
-#include <iostream>
-#include <map>
-#include <string>
-#include <typeinfo>
-#include <vector>
-
-using namespace std;
-using namespace cvc5;
-using namespace cvc5::parser;
-
-void translate_to_qepcad(
- string input,
- const vector<string>& info_tags,
- const vector<string>& info_data,
- const map<Expr, unsigned>& variables,
- const vector<Expr>& assertions);
-
-int main(int argc, char* argv[])
-{
- std::map<Expr, unsigned> 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> solver =
- std::unique_ptr<Solver>(new Solver(&options));
-
- // Create the parser
- ParserBuilder parserBuilder(solver.get(), input, options);
- Parser* parser = parserBuilder.build();
-
- // Variables and assertions
- std::map<Expr, unsigned> variables;
- vector<string> info_tags;
- vector<string> info_data;
- vector<Expr> assertions;
-
- Command* cmd;
- while ((cmd = parser->nextCommand())) {
-
- SetInfoCommand* setinfo = dynamic_cast<SetInfoCommand*>(cmd);
- if (setinfo) {
- info_tags.push_back(setinfo->getFlag());
- info_data.push_back(setinfo->getSExpr().getValue());
- delete cmd;
- continue;
- }
-
- DeclareFunctionCommand* declare =
- dynamic_cast<DeclareFunctionCommand*>(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<AssertCommand*>(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<Expr, unsigned>& variables,
- const Expr& term)
-{
- bool first;
-
- unsigned n = term.getNumChildren();
-
- if (n == 0) {
- if (term.getKind() == kind::CONST_RATIONAL) {
- cout << term.getConst<Rational>();
- } 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<Expr, unsigned>& 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<string>& info_tags,
- const vector<string>& info_data,
- const std::map<Expr, unsigned>& variables,
- const vector<Expr>& 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;
-}
+++ /dev/null
-/******************************************************************************
- * 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 <cvc5/cvc5.h>
-
-#include <cassert>
-#include <iostream>
-#include <map>
-#include <string>
-#include <typeinfo>
-#include <vector>
-
-using namespace std;
-using namespace cvc5;
-using namespace cvc5::parser;
-using namespace cvc5::options;
-
-void translate_to_redlog(
- string input,
- string command,
- const vector<string>& info_tags,
- const vector<string>& info_data,
- const map<Expr, unsigned>& variables,
- const vector<Expr>& 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> solver =
- std::unique_ptr<Solver>(new Solver(&options));
-
- // Create the parser
- ParserBuilder parserBuilder(solver.get(), input, options);
- Parser* parser = parserBuilder.build();
-
- // Variables and assertions
- std::map<Expr, unsigned> variables;
- vector<string> info_tags;
- vector<string> info_data;
- vector<Expr> assertions;
-
- Command* cmd;
- while ((cmd = parser->nextCommand())) {
-
- SetInfoCommand* setinfo = dynamic_cast<SetInfoCommand*>(cmd);
- if (setinfo) {
- info_tags.push_back(setinfo->getFlag());
- info_data.push_back(setinfo->getSExpr().getValue());
- delete cmd;
- continue;
- }
-
- DeclareFunctionCommand* declare = dynamic_cast<DeclareFunctionCommand*>(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<AssertCommand*>(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<Expr, unsigned>& variables, const Expr& term) {
- bool first;
-
- unsigned n = term.getNumChildren();
-
- if (n == 0) {
- if (term.getKind() == kind::CONST_RATIONAL) {
- cout << term.getConst<Rational>();
- } 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<Expr, unsigned>& variables, const Expr& assertion) {
- bool first;
-
- unsigned n = assertion.getNumChildren();
-
- if (n == 0) {
- if (assertion.isConst()) {
- if (assertion.getConst<bool>()) {
- 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<string>& info_tags,
- const vector<string>& info_data,
- const std::map<Expr, unsigned>& variables,
- const vector<Expr>& 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;
-
-}
+++ /dev/null
-###############################################################################
-# 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()
-
+++ /dev/null
-(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)
-
+++ /dev/null
-/******************************************************************************
- * 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 <cvc5/cvc5.h>
-#include <cvc4/options/set_language.h>
-
-#include <boost/algorithm/string.hpp> // include Boost, a C++ library
-#include <cassert>
-#include <iostream>
-#include <string>
-#include <typeinfo>
-#include <unordered_map>
-#include <vector>
-
-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<Type, Kind>, 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<Type> t_t;
- t_t.push_back(t);
- t_t.push_back(t);
- vector<Type> 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<Expr> 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 = "<stdin>";
- }
-
- // 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> solver =
- std::unique_ptr<Solver>(new Solver(&options));
-
- Mapper m(solver->getExprManager());
-
- // Create the parser
- ParserBuilder parserBuilder(solver.get(), input, options);
- if(input == "<stdin>") parserBuilder.withStreamInput(cin);
- std::unique_ptr<Parser> parser;
- parser.reset(parserBuilder.build());
-
- // Variables and assertions
- vector<string> variables;
- vector<string> info_tags;
- vector<string> info_data;
- vector<Expr> 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<SetBenchmarkLogicCommand*>(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<DeclareTypeCommand*>(cmd);
- DefineTypeCommand* definesort = dynamic_cast<DefineTypeCommand*>(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<AssertCommand*>(cmd);
- DeclareFunctionCommand* declarefun = dynamic_cast<DeclareFunctionCommand*>(cmd);
- DefineFunctionCommand* definefun = dynamic_cast<DefineFunctionCommand*>(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;
- }
-}
+++ /dev/null
-(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)
-
+++ /dev/null
-/******************************************************************************
- * 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 <cvc5/cvc5.h>
-#include <cvc4/expr/expr_iomanip.h>
-#include <cvc4/options/set_language.h>
-#include <getopt.h>
-
-#include <cerrno>
-#include <cstdlib>
-#include <cstring>
-#include <fstream>
-#include <iostream>
-
-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> solver = std::unique_ptr<Solver>(new Solver(&opts));
- ParserBuilder parserBuilder(solver.get(), filename, opts);
- if(!strcmp(filename, "-")) {
- parserBuilder.withFilename("<stdin>");
- 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<Expr> assertions;
- while(Command* cmd = parser->nextCommand()) {
- if(expand_definitions && dynamic_cast<DefineFunctionCommand*>(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<AssertCommand*>(cmd) != NULL) {
- Expr e = static_cast<AssertCommand*>(cmd)->getExpr();
- delete cmd;
- cmd = new AssertCommand(smt->expandDefinitions(e));
- } else if(expand_definitions && dynamic_cast<QueryCommand*>(cmd) != NULL) {
- Expr e = static_cast<QueryCommand*>(cmd)->getExpr();
- delete cmd;
- cmd = new QueryCommand(smt->expandDefinitions(e));
- } else if(expand_definitions && dynamic_cast<CheckSatCommand*>(cmd) != NULL) {
- Expr e = static_cast<CheckSatCommand*>(cmd)->getExpr();
- delete cmd;
- cmd = new CheckSatCommand(smt->expandDefinitions(e));
- } else if(expand_definitions && dynamic_cast<SimplifyCommand*>(cmd) != NULL) {
- Expr e = static_cast<SimplifyCommand*>(cmd)->getTerm();
- delete cmd;
- cmd = new SimplifyCommand(smt->expandDefinitions(e));
- } else if(expand_definitions && dynamic_cast<ExpandDefinitionsCommand*>(cmd) != NULL) {
- Expr e = static_cast<ExpandDefinitionsCommand*>(cmd)->getTerm();
- delete cmd;
- cmd = new ExpandDefinitionsCommand(smt->expandDefinitions(e));
- } else if(expand_definitions && dynamic_cast<GetValueCommand*>(cmd) != NULL) {
- vector<Expr> terms = static_cast<GetValueCommand*>(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<AssertCommand*>(cmd) != NULL) {
- // store up the assertion, don't print it yet
- assertions.push_back(static_cast<AssertCommand*>(cmd)->getExpr());
- } else {
- if(combine_assertions &&
- ( dynamic_cast<CheckSatCommand*>(cmd) != NULL ||
- dynamic_cast<QueryCommand*>(cmd) != NULL ||
- dynamic_cast<PushCommand*>(cmd) != NULL ||
- dynamic_cast<PopCommand*>(cmd) != NULL ||
- dynamic_cast<SimplifyCommand*>(cmd) != NULL ||
- dynamic_cast<QuitCommand*>(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<QuitCommand*>(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;
-}
projects / cvc5.git / commitdiff