From 41d07960fd817d0d98b6bf65b2b3c2687837e46c Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 14 Jun 2021 16:45:17 -0700 Subject: Final update to SMT-COMP 2021 options (#6739) This commit: - Disables `--tear-down-incremental=X` for the competition since it currently does not work correctly on master and a fixed version did not show significant benefits. - Changes the occurrences of `--nl-ext` to `--nl-ext=full` because it is now a mode option. - Removes the use of `--bv-assert-input` because the option currently has some issues in incremental mode (#6738) - Removes the use of `--bitblast=eager` for the model validation track because it produces invalid models (#6741) --- .../smt-comp/run-script-smtcomp-current | 12 +++---- .../run-script-smtcomp-current-incremental | 40 +++------------------- .../run-script-smtcomp-current-model-validation | 4 +-- .../run-script-smtcomp-current-unsat-cores | 7 ++-- 4 files changed, 15 insertions(+), 48 deletions(-) diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current index ecc6ce5fe..9b4f534b0 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current @@ -1,6 +1,6 @@ #!/bin/bash -cvc5=./cvc5 +cvc5=$(dirname "$(readlink -f "$0")")/cvc5 bench="$1" # Output other than "sat"/"unsat" is either written to stderr or to "err.log" @@ -75,7 +75,7 @@ QF_NRA) finishwith --decision=internal --nl-ext=none ;; # all logics with UF + quantifiers should either fall under this or special cases below -ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUFBVDTLIA|AUFNIA|UFFPDTLIRA|UFFPDTNIRA) +ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFBVLIA|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUFBV|AUFBVDTLIA|AUFBVFP|AUFNIA|UFFPDTLIRA|UFFPDTNIRA) # initial runs 1 min trywith 30 --simplification=none --full-saturate-quant trywith 30 --no-e-matching --full-saturate-quant @@ -112,7 +112,7 @@ UFBV) trywith 30 --full-saturate-quant --no-cegqi-innermost --global-negate finishwith --finite-model-find ;; -BV) +ABV|BV) trywith 120 --full-saturate-quant trywith 120 --sygus-inst trywith 300 --full-saturate-quant --cegqi-nested-qe --decision=internal @@ -121,7 +121,7 @@ BV) # finish 10min finishwith --full-saturate-quant --no-cegqi-innermost --global-negate ;; -ABVFP|BVFP|FP|NIA|NRA) +ABVFP|ABVFPLRA|BVFP|FP|NIA|NRA) trywith 300 --full-saturate-quant --nl-ext-tplanes --fp-exp finishwith --sygus-inst --fp-exp ;; @@ -131,8 +131,8 @@ LIA|LRA) finishwith --full-saturate-quant --cegqi-nested-qe --decision=internal ;; QF_AUFBV) - trywith 600 --ite-simp - finishwith --decision=justification-stoponly --ite-simp + trywith 600 + finishwith --decision=justification-stoponly ;; QF_ABV) trywith 50 --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental b/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental index 21bb2f6e0..79df91d69 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental @@ -1,6 +1,6 @@ #!/bin/bash -cvc5=./cvc5 +cvc5=$(dirname "$(readlink -f "$0")")/cvc5 line="" while [[ -z "$line" ]]; do @@ -26,50 +26,20 @@ function runcvc5 { # we run in this way for line-buffered input, otherwise memory's a # concern (plus it mimics what we'll end up getting from an # application-track trace runner?) - $cvc5 --force-logic="$logic" -L smt2.6 --print-success --no-type-checking --no-interactive "$@" <&0- + $cvc5 --incremental --force-logic="$logic" -L smt2.6 --print-success --no-type-checking --no-interactive "$@" <&0- } case "$logic" in -ALIA|ANIA|AUFNIRA|LIA|LRA|QF_ALIA|QF_ANIA|QF_AUFBVLIA|QF_AUFBVNIA|QF_LIA|QF_LRA|QF_NIA|QF_UFBVLIA|QF_UFLIA|QF_UFLRA|QF_UFNIA|UFLRA) - runcvc5 --tear-down-incremental=1 - ;; QF_AUFLIA) - runcvc5 --tear-down-incremental=1 --no-arrays-eager-index --arrays-eager-lemmas + runcvc5 --no-arrays-eager-index --arrays-eager-lemmas ;; QF_BV) - runcvc5 --incremental --bitblast=eager --bv-assert-input - ;; -QF_UFBV) - runcvc5 --incremental --bv-assert-input - ;; -QF_UF) - runcvc5 --incremental - ;; -QF_AUFBV) - runcvc5 --incremental --bv-assert-input - ;; -QF_ABV) - runcvc5 --incremental --bv-assert-input - ;; -ABVFP) - runcvc5 --incremental - ;; -BVFP) - runcvc5 --incremental - ;; -QF_ABVFP) - runcvc5 --incremental - ;; -QF_BVFP) - runcvc5 --incremental - ;; -QF_FP) - runcvc5 --incremental + runcvc5 --bitblast=eager ;; *) # just run the default - runcvc5 --incremental + runcvc5 ;; esac diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation b/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation index fe8d4ae44..0998e9949 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation @@ -1,6 +1,6 @@ #!/bin/bash -cvc5=./cvc5 +cvc5=$(dirname "$(readlink -f "$0")")/cvc5 bench="$1" logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic *\([A-Z_]*\) *) *$') @@ -20,7 +20,7 @@ QF_LIA) finishwith --miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --use-soi --pb-rewrites --ite-simp --simp-ite-compress ;; QF_BV) - finishwith --bitblast=eager --bv-assert-input + finishwith --bv-assert-input ;; *) # just run the default diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores b/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores index e9753781d..75e3bfc82 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores @@ -1,6 +1,6 @@ #!/bin/bash -cvc5=./cvc5 +cvc5=$(dirname "$(readlink -f "$0")")/cvc5 bench="$1" logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic *\([A-Z_]*\) *) *$') @@ -20,10 +20,7 @@ QF_LIA) finishwith --miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --use-soi ;; QF_NIA) - finishwith --nl-ext --nl-ext-tplanes - ;; -QF_NRA) - finishwith --nl-ext --nl-ext-tplanes + finishwith --nl-ext-tplanes ;; # all logics with UF + quantifiers should either fall under this or special cases below ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUFBVDTLIA|AUFNIA|ABVFP|BVFP|FP) -- cgit v1.2.3 From ac0146e4142587df45dada4bdf9e0d0faec81a67 Mon Sep 17 00:00:00 2001 From: yoni206 Date: Tue, 15 Jun 2021 09:28:40 -0700 Subject: An example for a quick start guide (#6686) Co-authored-by: Aina Niemetz --- examples/api/cpp/CMakeLists.txt | 1 + examples/api/cpp/quickstart.cpp | 170 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 171 insertions(+) create mode 100644 examples/api/cpp/quickstart.cpp diff --git a/examples/api/cpp/CMakeLists.txt b/examples/api/cpp/CMakeLists.txt index bff7caa4d..6f66fdc5f 100644 --- a/examples/api/cpp/CMakeLists.txt +++ b/examples/api/cpp/CMakeLists.txt @@ -24,6 +24,7 @@ set(CVC5_EXAMPLES_API sets sequences strings + quickstart ) foreach(example ${CVC5_EXAMPLES_API}) diff --git a/examples/api/cpp/quickstart.cpp b/examples/api/cpp/quickstart.cpp new file mode 100644 index 000000000..5d4849bc0 --- /dev/null +++ b/examples/api/cpp/quickstart.cpp @@ -0,0 +1,170 @@ +/****************************************************************************** + * Top contributors (to current version): + * Yoni Zohar + * + * 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. + * **************************************************************************** + * + * A simple demonstration of the api capabilities of cvc5. + * + */ + +#include + +#include + +using namespace std; +using namespace cvc5::api; + +int main() +{ + // Create a solver + Solver solver; + + // We will ask the solver to produce models and unsat cores, + // hence these options should be turned on. + solver.setOption("produce-models", "true"); + solver.setOption("produce-unsat-cores", "true"); + + // The simplest way to set a logic for the solver is to choose "ALL". + // This enables all logics in the solver. + // Alternatively, "QF_ALL" enables all logics without quantifiers. + // To optimize the solver's behavior for a more specific logic, + // use the logic name, e.g. "QF_BV" or "QF_AUFBV". + + // Set the logic + solver.setLogic("ALL"); + + // In this example, we will define constraints over reals and integers. + // Hence, we first obtain the corresponding sorts. + Sort realSort = solver.getRealSort(); + Sort intSort = solver.getIntegerSort(); + + // x and y will be real variables, while a and b will be integer variables. + // Formally, their cpp type is Term, + // and they are called "constants" in SMT jargon: + Term x = solver.mkConst(realSort, "x"); + Term y = solver.mkConst(realSort, "y"); + Term a = solver.mkConst(intSort, "a"); + Term b = solver.mkConst(intSort, "b"); + + // Our constraints regarding x and y will be: + // + // (1) 0 < x + // (2) 0 < y + // (3) x + y < 1 + // (4) x <= y + // + + // Formally, constraints are also terms. Their sort is Boolean. + // We will construct these constraints gradually, + // by defining each of their components. + // We start with the constant numerals 0 and 1: + Term zero = solver.mkReal(0); + Term one = solver.mkReal(1); + + // Next, we construct the term x + y + Term xPlusY = solver.mkTerm(PLUS, x, y); + + // Now we can define the constraints. + // They use the operators +, <=, and <. + // In the API, these are denoted by PLUS, LEQ, and LT. + // A list of available operators is available in: + // src/api/cpp/cvc5_kind.h + Term constraint1 = solver.mkTerm(LT, zero, x); + Term constraint2 = solver.mkTerm(LT, zero, y); + Term constraint3 = solver.mkTerm(LT, xPlusY, one); + Term constraint4 = solver.mkTerm(LEQ, x, y); + + // Now we assert the constraints to the solver. + solver.assertFormula(constraint1); + solver.assertFormula(constraint2); + solver.assertFormula(constraint3); + solver.assertFormula(constraint4); + + // Check if the formula is satisfiable, that is, + // are there real values for x,y,z that satisfy all the constraints? + Result r1 = solver.checkSat(); + + // The result is either SAT, UNSAT, or UNKNOWN. + // In this case, it is SAT. + std::cout << "expected: sat" << std::endl; + std::cout << "result:" << r1 << std::endl; + + // We can get the values for x and y that satisfy the constraints. + Term xVal = solver.getValue(x); + Term yVal = solver.getValue(y); + + // It is also possible to get values for compound terms, + // even if those did not appear in the original formula. + Term xMinusY = solver.mkTerm(MINUS, x, y); + Term xMinusYVal = solver.getValue(xMinusY); + + // We can now obtain thestring representations of the values. + std::string xStr = xVal.getRealValue(); + std::string yStr = yVal.getRealValue(); + std::string xMinusYStr = xMinusYVal.getRealValue(); + + std::cout << "value for x: " << xStr << std::endl; + std::cout << "value for y: " << yStr << std::endl; + std::cout << "value for x - y: " << xMinusYStr << std::endl; + + // Further, we can convert the values to cpp types, + // using standard cpp conversion functions. + double xDouble = std::stod(xStr); + double yDouble = std::stod(yStr); + double xMinusYDouble = std::stod(xMinusYStr); + + // Another way to independently compute the value of x and y would be using + // the ordinary cpp minus operator instead of asking the solver. + // However, for more complex terms, + // it is easier to let the solver do the evaluation. + double xMinusYComputed = xDouble - yDouble; + if (xMinusYComputed == xMinusYDouble) + { + std::cout << "computed correctly" << std::endl; + } + else + { + std::cout << "computed incorrectly" << std::endl; + } + + // Next, we will check satisfiability of the same formula, + // only this time over integer variables a and b. + + // We start by resetting assertions added to the solver. + solver.resetAssertions(); + + // Next, we assert the same assertions above with integers. + // This time, we inline the construction of terms + // to the assertion command. + solver.assertFormula(solver.mkTerm(LT, solver.mkInteger(0), a)); + solver.assertFormula(solver.mkTerm(LT, solver.mkInteger(0), b)); + solver.assertFormula( + solver.mkTerm(LT, solver.mkTerm(PLUS, a, b), solver.mkInteger(1))); + solver.assertFormula(solver.mkTerm(LEQ, a, b)); + + // We check whether the revised assertion is satisfiable. + Result r2 = solver.checkSat(); + + // This time the formula is unsatisfiable + std::cout << "expected: unsat" << std::endl; + std::cout << "result: " << r2 << std::endl; + + // We can query the solver for an unsatisfiable core, i.e., a subset + // of the assertions that is already unsatisfiable. + std::vector unsatCore = solver.getUnsatCore(); + std::cout << "unsat core size: " << unsatCore.size() << std::endl; + std::cout << "unsat core: " << std::endl; + for (const Term& t : unsatCore) + { + std::cout << t << std::endl; + } + + return 0; +} -- cgit v1.2.3 From 786574dff56615972fe89fca81c4f7a517ef16d9 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 15 Jun 2021 10:30:07 -0700 Subject: docs: Add references instead of links in theory reference pages. (#6729) --- docs/references.bib | 93 ++++++++++++++++++++++++++++++++++++ docs/theories/datatypes.rst | 8 ++-- docs/theories/separation-logic.rst | 7 ++- docs/theories/sets-and-relations.rst | 6 +-- 4 files changed, 102 insertions(+), 12 deletions(-) diff --git a/docs/references.bib b/docs/references.bib index 50e410e7b..8e3fd5e69 100644 --- a/docs/references.bib +++ b/docs/references.bib @@ -6,3 +6,96 @@ pages={1-84}, doi={10.1109/IEEESTD.2019.8766229} } + +@article{BansalBRT17, + author = {Kshitij Bansal and + Clark W. Barrett and + Andrew Reynolds and + Cesare Tinelli}, + title = {A New Decision Procedure for Finite Sets and Cardinality Constraints + in {SMT}}, + journal = {CoRR}, + volume = {abs/1702.06259}, + year = {2017}, + archivePrefix = {arXiv}, + eprint = {1702.06259}, + timestamp = {Mon, 13 Aug 2018 16:47:11 +0200}, + biburl = {https://dblp.org/rec/journals/corr/BansalBRT17.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{MengRTB17, + author = {Baoluo Meng and + Andrew Reynolds and + Cesare Tinelli and + Clark W. Barrett}, + editor = {Leonardo de Moura}, + title = {Relational Constraint Solving in {SMT}}, + booktitle = {Automated Deduction - {CADE} 26 - 26th International Conference on + Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings}, + series = {Lecture Notes in Computer Science}, + volume = {10395}, + pages = {148--165}, + publisher = {Springer}, + year = {2017}, + doi = {10.1007/978-3-319-63046-5_10}, + timestamp = {Wed, 25 Sep 2019 18:19:14 +0200}, + biburl = {https://dblp.org/rec/conf/cade/MengRTB17.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{ReynoldsISK16, + author = {Andrew Reynolds and + Radu Iosif and + Cristina Serban and + Tim King}, + editor = {Cyrille Artho and + Axel Legay and + Doron Peled}, + title = {A Decision Procedure for Separation Logic in {SMT}}, + booktitle = {Automated Technology for Verification and Analysis - 14th International + Symposium, {ATVA} 2016, Chiba, Japan, October 17-20, 2016, Proceedings}, + series = {Lecture Notes in Computer Science}, + volume = {9938}, + pages = {244--261}, + year = {2016}, + doi = {10.1007/978-3-319-46520-3_16}, + timestamp = {Tue, 14 May 2019 10:00:49 +0200}, + biburl = {https://dblp.org/rec/conf/atva/ReynoldsIS016.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{ReynoldsB15, + author = {Andrew Reynolds and + Jasmin Christian Blanchette}, + editor = {Amy P. Felty and + Aart Middeldorp}, + title = {A Decision Procedure for (Co)datatypes in {SMT} Solvers}, + booktitle = {Automated Deduction - {CADE-25} - 25th International Conference on + Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings}, + series = {Lecture Notes in Computer Science}, + volume = {9195}, + pages = {197--213}, + publisher = {Springer}, + year = {2015}, + doi = {10.1007/978-3-319-21401-6_13}, + timestamp = {Tue, 14 May 2019 10:00:39 +0200}, + biburl = {https://dblp.org/rec/conf/cade/ReynoldsB15.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@article{BarrettST07, + author = {Clark W. Barrett and + Igor Shikanian and + Cesare Tinelli}, + title = {An Abstract Decision Procedure for a Theory of Inductive Data Types}, + journal = {J. Satisf. Boolean Model. Comput.}, + volume = {3}, + number = {1-2}, + pages = {21--46}, + year = {2007}, + doi = {10.3233/sat190028}, + timestamp = {Mon, 17 Aug 2020 18:32:39 +0200}, + biburl = {https://dblp.org/rec/journals/jsat/BarrettST07.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} diff --git a/docs/theories/datatypes.rst b/docs/theories/datatypes.rst index 5f02a8bf8..1211a43ee 100644 --- a/docs/theories/datatypes.rst +++ b/docs/theories/datatypes.rst @@ -45,8 +45,8 @@ evaluate to true iff their argument has top-symbol ``C``. Semantics --------- -The decision procedure for inductive datatypes can be found -`here `__. +The decision procedure for inductive datatypes is described in +:cite:`BarrettST07`. Example Declarations -------------------- @@ -150,8 +150,8 @@ For example: Codatatypes ----------- -cvc5 also supports co-inductive datatypes, as described -`here `__. +cvc5 also supports co-inductive datatypes, as described in +:cite:`ReynoldsB15`. The syntax for declaring mutually recursive coinductive datatype blocks is identical to inductive datatypes, except that ``declare-datatypes`` is replaced diff --git a/docs/theories/separation-logic.rst b/docs/theories/separation-logic.rst index c2dcda78e..43c114404 100644 --- a/docs/theories/separation-logic.rst +++ b/docs/theories/separation-logic.rst @@ -7,10 +7,9 @@ language. Signature --------- -Given a (decidable) base theory :math:`T`, cvc5 has a -`decision procedure `__ -for quantifier-free :math:`SL(T)_{Loc,Data}` formulas, where :math:`Loc` and -:math:`Data` are any sort belonging to :math:`T`. +Given a (decidable) base theory :math:`T`, cvc5 implements a decision procedure +for quantifier-free :math:`SL(T)_{Loc,Data}` formulas :cite:`ReynoldsIS016`, +where :math:`Loc` and :math:`Data` are any sort belonging to :math:`T`. A :math:`SL(T)_{Loc,Data}` formula is one from the following grammar: diff --git a/docs/theories/sets-and-relations.rst b/docs/theories/sets-and-relations.rst index 79838334f..88671a837 100644 --- a/docs/theories/sets-and-relations.rst +++ b/docs/theories/sets-and-relations.rst @@ -20,8 +20,7 @@ The source code of these examples is available at: Below is a short summary of the sorts, constants, functions and -predicates. For more details, see -`this paper at IJCAR 2016 `__. +predicates. More details can be found in :cite:`BansalBRT17`. For the C++ API examples in the table below, we assume that we have created a `cvc5::api::Solver solver` object. @@ -151,8 +150,7 @@ Example: For reference, below is a short summary of the sorts, constants, functions and predicates. -For more details, see -`this paper at CADE 2017 `__. +More details can be found in :cite:`MengRTB17`. +----------------------+----------------------------------------------+------------------------------------------------------------------------------------+ | | SMTLIB language | C++ API | -- cgit v1.2.3 From 59bbcb5aa51b2ae9689e69afb05b017ee4fcb43a Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Tue, 15 Jun 2021 15:29:08 -0300 Subject: CVC4 -> cvc5 in cpp API examples (#6746) --- examples/api/cpp/bitvectors.cpp | 22 +++++++++++----------- examples/api/cpp/bitvectors_and_arrays.cpp | 6 +++--- examples/api/cpp/datatypes.cpp | 6 +++--- examples/api/cpp/extract.cpp | 4 ++-- examples/api/cpp/helloworld.cpp | 2 +- examples/api/cpp/linear_arith.cpp | 14 +++++++------- examples/api/cpp/sequences.cpp | 4 ++-- examples/api/cpp/sets.cpp | 6 +++--- examples/api/cpp/strings.cpp | 4 ++-- 9 files changed, 34 insertions(+), 34 deletions(-) diff --git a/examples/api/cpp/bitvectors.cpp b/examples/api/cpp/bitvectors.cpp index 8768bd996..51f438a2d 100644 --- a/examples/api/cpp/bitvectors.cpp +++ b/examples/api/cpp/bitvectors.cpp @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * A simple demonstration of the solving capabilities of the CVC4 + * A simple demonstration of the solving capabilities of the cvc5 * bit-vector solver. * */ @@ -43,7 +43,7 @@ int main() // //(2) x = a + b - x; // - // We will use CVC4 to prove that the three pieces of code above are all + // We will use cvc5 to prove that the three pieces of code above are all // equivalent by encoding the problem in the bit-vector theory. // Creating a bit-vector type of width 32 @@ -73,7 +73,7 @@ int main() Term assignment0 = slv.mkTerm(EQUAL, new_x, ite); // Assert the encoding of code (0) - cout << "Asserting " << assignment0 << " to CVC4 " << endl; + cout << "Asserting " << assignment0 << " to cvc5 " << endl; slv.assertFormula(assignment0); cout << "Pushing a new context." << endl; slv.push(); @@ -83,14 +83,14 @@ int main() Term a_xor_b_xor_x = slv.mkTerm(BITVECTOR_XOR, a, b, x); Term assignment1 = slv.mkTerm(EQUAL, new_x_, a_xor_b_xor_x); - // Assert encoding to CVC4 in current context; - cout << "Asserting " << assignment1 << " to CVC4 " << endl; + // Assert encoding to cvc5 in current context; + cout << "Asserting " << assignment1 << " to cvc5 " << endl; slv.assertFormula(assignment1); Term new_x_eq_new_x_ = slv.mkTerm(EQUAL, new_x, new_x_); cout << " Check entailment assuming: " << new_x_eq_new_x_ << endl; cout << " Expect ENTAILED. " << endl; - cout << " CVC4: " << slv.checkEntailed(new_x_eq_new_x_) << endl; + cout << " cvc5: " << slv.checkEntailed(new_x_eq_new_x_) << endl; cout << " Popping context. " << endl; slv.pop(); @@ -100,19 +100,19 @@ int main() Term a_plus_b_minus_x = slv.mkTerm(BITVECTOR_SUB, a_plus_b, x); Term assignment2 = slv.mkTerm(EQUAL, new_x_, a_plus_b_minus_x); - // Assert encoding to CVC4 in current context; - cout << "Asserting " << assignment2 << " to CVC4 " << endl; + // Assert encoding to cvc5 in current context; + cout << "Asserting " << assignment2 << " to cvc5 " << endl; slv.assertFormula(assignment2); cout << " Check entailment assuming: " << new_x_eq_new_x_ << endl; cout << " Expect ENTAILED. " << endl; - cout << " CVC4: " << slv.checkEntailed(new_x_eq_new_x_) << endl; + cout << " cvc5: " << slv.checkEntailed(new_x_eq_new_x_) << endl; Term x_neq_x = slv.mkTerm(EQUAL, x, x).notTerm(); std::vector v{new_x_eq_new_x_, x_neq_x}; cout << " Check entailment assuming: " << v << endl; cout << " Expect NOT_ENTAILED. " << endl; - cout << " CVC4: " << slv.checkEntailed(v) << endl; + cout << " cvc5: " << slv.checkEntailed(v) << endl; // Assert that a is odd Op extract_op = slv.mkOp(BITVECTOR_EXTRACT, 0, 0); @@ -123,6 +123,6 @@ int main() cout << "Check satisfiability." << endl; slv.assertFormula(a_odd); cout << " Expect sat. " << endl; - cout << " CVC4: " << slv.checkSat() << endl; + cout << " cvc5: " << slv.checkSat() << endl; return 0; } diff --git a/examples/api/cpp/bitvectors_and_arrays.cpp b/examples/api/cpp/bitvectors_and_arrays.cpp index 547b294a0..6b58daf1b 100644 --- a/examples/api/cpp/bitvectors_and_arrays.cpp +++ b/examples/api/cpp/bitvectors_and_arrays.cpp @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * A simple demonstration of the solving capabilities of the CVC4 + * A simple demonstration of the solving capabilities of the cvc5 * bit-vector and array solvers. * */ @@ -84,10 +84,10 @@ int main() Term query = slv.mkTerm(NOT, slv.mkTerm(AND, assertions)); - cout << "Asserting " << query << " to CVC4 " << endl; + cout << "Asserting " << query << " to cvc5 " << endl; slv.assertFormula(query); cout << "Expect sat. " << endl; - cout << "CVC4: " << slv.checkSatAssuming(slv.mkTrue()) << endl; + cout << "cvc5: " << slv.checkSatAssuming(slv.mkTrue()) << endl; // Getting the model cout << "The satisfying model is: " << endl; diff --git a/examples/api/cpp/datatypes.cpp b/examples/api/cpp/datatypes.cpp index 76c6da0f0..1ba9beaf1 100644 --- a/examples/api/cpp/datatypes.cpp +++ b/examples/api/cpp/datatypes.cpp @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * An example of using inductive datatypes in CVC4. + * An example of using inductive datatypes in cvc5. */ #include @@ -127,7 +127,7 @@ void test(Solver& slv, Sort& consListSort) std::cout << "Assert " << assertion << std::endl; slv.assertFormula(assertion); std::cout << "Expect sat." << std::endl; - std::cout << "CVC4: " << slv.checkSat() << std::endl; + std::cout << "cvc5: " << slv.checkSat() << std::endl; } int main() @@ -153,7 +153,7 @@ int main() std::cout << "spec is:" << std::endl << consListSpec << std::endl; // Keep in mind that "DatatypeDecl" is the specification class for - // datatypes---"DatatypeDecl" is not itself a CVC4 Sort. + // datatypes---"DatatypeDecl" is not itself a cvc5 Sort. // Now that our Datatype is fully specified, we can get a Sort for it. // This step resolves the "SelfSort" reference and creates // symbols for all the constructors, etc. diff --git a/examples/api/cpp/extract.cpp b/examples/api/cpp/extract.cpp index d21c59d59..b5de58d26 100644 --- a/examples/api/cpp/extract.cpp +++ b/examples/api/cpp/extract.cpp @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * A simple demonstration of the solving capabilities of the CVC4 + * A simple demonstration of the solving capabilities of the cvc5 * bit-vector solver. * */ @@ -50,7 +50,7 @@ int main() Term eq2 = slv.mkTerm(EQUAL, x_31_31, x_0_0); cout << " Check entailment assuming: " << eq2 << endl; cout << " Expect ENTAILED. " << endl; - cout << " CVC4: " << slv.checkEntailed(eq2) << endl; + cout << " cvc5: " << slv.checkEntailed(eq2) << endl; return 0; } diff --git a/examples/api/cpp/helloworld.cpp b/examples/api/cpp/helloworld.cpp index 21eb8e8fc..3d11d1bd0 100644 --- a/examples/api/cpp/helloworld.cpp +++ b/examples/api/cpp/helloworld.cpp @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * A very simple CVC4 example. + * A very simple cvc5 example. */ #include diff --git a/examples/api/cpp/linear_arith.cpp b/examples/api/cpp/linear_arith.cpp index 02ddd956c..979959d21 100644 --- a/examples/api/cpp/linear_arith.cpp +++ b/examples/api/cpp/linear_arith.cpp @@ -11,7 +11,7 @@ * **************************************************************************** * * A simple demonstration of the linear arithmetic solving capabilities and - * the push pop of CVC4. This also gives an example option. + * the push pop of cvc5. This also gives an example option. */ #include @@ -60,9 +60,9 @@ int main() slv.push(); Term diff_leq_two_thirds = slv.mkTerm(LEQ, diff, two_thirds); - cout << "Prove that " << diff_leq_two_thirds << " with CVC4." << endl; - cout << "CVC4 should report ENTAILED." << endl; - cout << "Result from CVC4 is: " << slv.checkEntailed(diff_leq_two_thirds) + cout << "Prove that " << diff_leq_two_thirds << " with cvc5." << endl; + cout << "cvc5 should report ENTAILED." << endl; + cout << "Result from cvc5 is: " << slv.checkEntailed(diff_leq_two_thirds) << endl; slv.pop(); @@ -72,9 +72,9 @@ int main() Term diff_is_two_thirds = slv.mkTerm(EQUAL, diff, two_thirds); slv.assertFormula(diff_is_two_thirds); cout << "Show that the assertions are consistent with " << endl; - cout << diff_is_two_thirds << " with CVC4." << endl; - cout << "CVC4 should report SAT." << endl; - cout << "Result from CVC4 is: " << slv.checkSat() << endl; + cout << diff_is_two_thirds << " with cvc5." << endl; + cout << "cvc5 should report SAT." << endl; + cout << "Result from cvc5 is: " << slv.checkSat() << endl; slv.pop(); cout << "Thus the maximum value of (y - x) is 2/3."<< endl; diff --git a/examples/api/cpp/sequences.cpp b/examples/api/cpp/sequences.cpp index 5ee66048f..40cacf5c7 100644 --- a/examples/api/cpp/sequences.cpp +++ b/examples/api/cpp/sequences.cpp @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * A simple demonstration of reasoning about sequences with CVC4 via C++ API. + * A simple demonstration of reasoning about sequences with cvc5 via C++ API. */ #include @@ -57,7 +57,7 @@ int main() // check sat Result result = slv.checkSatAssuming(q); - std::cout << "CVC4 reports: " << q << " is " << result << "." << std::endl; + std::cout << "cvc5 reports: " << q << " is " << result << "." << std::endl; if (result.isSat()) { diff --git a/examples/api/cpp/sets.cpp b/examples/api/cpp/sets.cpp index c1eded4a4..1f3a1683c 100644 --- a/examples/api/cpp/sets.cpp +++ b/examples/api/cpp/sets.cpp @@ -51,7 +51,7 @@ int main() Term theorem = slv.mkTerm(EQUAL, lhs, rhs); - cout << "CVC4 reports: " << theorem << " is " << slv.checkEntailed(theorem) + cout << "cvc5 reports: " << theorem << " is " << slv.checkEntailed(theorem) << "." << endl; } @@ -62,7 +62,7 @@ int main() Term theorem = slv.mkTerm(SUBSET, emptyset, A); - cout << "CVC4 reports: " << theorem << " is " << slv.checkEntailed(theorem) + cout << "cvc5 reports: " << theorem << " is " << slv.checkEntailed(theorem) << "." << endl; } @@ -84,7 +84,7 @@ int main() Term e = slv.mkTerm(MEMBER, x, intersection); Result result = slv.checkSatAssuming(e); - cout << "CVC4 reports: " << e << " is " << result << "." << endl; + cout << "cvc5 reports: " << e << " is " << result << "." << endl; if (result.isSat()) { diff --git a/examples/api/cpp/strings.cpp b/examples/api/cpp/strings.cpp index a952b31d1..01e384ee7 100644 --- a/examples/api/cpp/strings.cpp +++ b/examples/api/cpp/strings.cpp @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * A simple demonstration of reasoning about strings with CVC4 via C++ API. + * A simple demonstration of reasoning about strings with cvc5 via C++ API. */ #include @@ -84,7 +84,7 @@ int main() // check sat Result result = slv.checkSatAssuming(q); - std::cout << "CVC4 reports: " << q << " is " << result << "." << std::endl; + std::cout << "cvc5 reports: " << q << " is " << result << "." << std::endl; if(result.isSat()) { -- cgit v1.2.3 From 09e438c6e6d10e0ad1e7c3e3de39ed4eb1d48ee1 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 15 Jun 2021 11:46:22 -0700 Subject: docs: Fix reference in sep logic reference. (#6747) --- docs/theories/separation-logic.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/theories/separation-logic.rst b/docs/theories/separation-logic.rst index 43c114404..86f802ef8 100644 --- a/docs/theories/separation-logic.rst +++ b/docs/theories/separation-logic.rst @@ -8,7 +8,7 @@ Signature --------- Given a (decidable) base theory :math:`T`, cvc5 implements a decision procedure -for quantifier-free :math:`SL(T)_{Loc,Data}` formulas :cite:`ReynoldsIS016`, +for quantifier-free :math:`SL(T)_{Loc,Data}` formulas :cite:`ReynoldsISK16`, where :math:`Loc` and :math:`Data` are any sort belonging to :math:`T`. A :math:`SL(T)_{Loc,Data}` formula is one from the following grammar: -- cgit v1.2.3 From 6bae871954c48993009ed91d4b907c136017ed38 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 15 Jun 2021 22:30:19 +0200 Subject: Remove public option wrappers (#6716) This PR gets rid of almost all remaining public option wrappers. It does so by - making base, main and parser options public such that they can directly be used from the driver and the parser - moving incremental and the resource limiting options to base - moving dumping options to main After this PR, the only option wrapper left is becoming obsolete as well after (the follow-up of) #6697. --- src/api/cpp/cvc5.cpp | 17 ++--- src/main/command_executor.cpp | 43 +++++------ src/main/driver_unified.cpp | 72 +++++++++---------- src/main/interactive_shell.cpp | 17 ++--- src/main/main.cpp | 16 ++--- src/main/time_limit.cpp | 4 +- src/options/CMakeLists.txt | 1 - src/options/base_options.toml | 59 +++++++++++++++ src/options/main_options.toml | 48 +++++++++++++ src/options/options_handler.cpp | 3 +- src/options/options_public.cpp | 108 ---------------------------- src/options/options_public.h | 36 ---------- src/options/parser_options.toml | 1 + src/options/resource_manager_options.toml | 51 ------------- src/options/smt_options.toml | 57 --------------- src/parser/parser.cpp | 4 +- src/parser/parser_builder.cpp | 17 ++--- src/parser/smt2/smt2.cpp | 3 +- src/preprocessing/passes/ackermann.cpp | 2 +- src/preprocessing/passes/int_to_bv.cpp | 1 + src/preprocessing/passes/ite_simp.cpp | 1 + src/preprocessing/passes/miplib_trick.cpp | 2 +- src/prop/minisat/core/Solver.cc | 1 + src/smt/command.cpp | 1 + src/smt/preprocessor.cpp | 1 + src/smt/set_defaults.cpp | 2 +- src/smt/smt_engine.cpp | 7 +- src/smt/smt_engine_state.cpp | 1 + src/smt/sygus_solver.cpp | 1 + src/theory/arith/arith_ite_utils.cpp | 1 + src/theory/arith/theory_arith_private.cpp | 2 +- src/theory/bv/bitblast/eager_bitblaster.cpp | 1 + src/theory/bv/bv_eager_solver.cpp | 1 + src/theory/quantifiers/instantiate.cpp | 1 + src/theory/quantifiers/term_registry.cpp | 1 + src/util/resource_manager.cpp | 36 +++++----- test/api/smt2_compliance.cpp | 5 +- 37 files changed, 248 insertions(+), 377 deletions(-) delete mode 100644 src/options/resource_manager_options.toml diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 668fc9382..307222988 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -55,6 +55,7 @@ #include "expr/sequence.h" #include "expr/type_node.h" #include "expr/uninterpreted_constant.h" +#include "options/base_options.h" #include "options/main_options.h" #include "options/option_exception.h" #include "options/options.h" @@ -6452,7 +6453,7 @@ Result Solver::checkEntailed(const Term& term) const NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK(!d_smtEngine->isQueryMade() - || d_smtEngine->getOptions().smt.incrementalSolving) + || d_smtEngine->getOptions().base.incrementalSolving) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC5_API_SOLVER_CHECK_TERM(term); @@ -6468,7 +6469,7 @@ Result Solver::checkEntailed(const std::vector& terms) const CVC5_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); CVC5_API_CHECK(!d_smtEngine->isQueryMade() - || d_smtEngine->getOptions().smt.incrementalSolving) + || d_smtEngine->getOptions().base.incrementalSolving) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC5_API_SOLVER_CHECK_TERMS(terms); @@ -6497,7 +6498,7 @@ Result Solver::checkSat(void) const CVC5_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); CVC5_API_CHECK(!d_smtEngine->isQueryMade() - || d_smtEngine->getOptions().smt.incrementalSolving) + || d_smtEngine->getOptions().base.incrementalSolving) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; //////// all checks before this line @@ -6512,7 +6513,7 @@ Result Solver::checkSatAssuming(const Term& assumption) const CVC5_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); CVC5_API_CHECK(!d_smtEngine->isQueryMade() - || d_smtEngine->getOptions().smt.incrementalSolving) + || d_smtEngine->getOptions().base.incrementalSolving) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC5_API_SOLVER_CHECK_TERM_WITH_SORT(assumption, getBooleanSort()); @@ -6528,7 +6529,7 @@ Result Solver::checkSatAssuming(const std::vector& assumptions) const CVC5_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); CVC5_API_CHECK(!d_smtEngine->isQueryMade() || assumptions.size() == 0 - || d_smtEngine->getOptions().smt.incrementalSolving) + || d_smtEngine->getOptions().base.incrementalSolving) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC5_API_SOLVER_CHECK_TERMS_WITH_SORT(assumptions, getBooleanSort()); @@ -6863,7 +6864,7 @@ std::vector Solver::getUnsatAssumptions(void) const { CVC5_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); - CVC5_API_CHECK(d_smtEngine->getOptions().smt.incrementalSolving) + CVC5_API_CHECK(d_smtEngine->getOptions().base.incrementalSolving) << "Cannot get unsat assumptions unless incremental solving is enabled " "(try --incremental)"; CVC5_API_CHECK(d_smtEngine->getOptions().smt.unsatAssumptions) @@ -7044,7 +7045,7 @@ void Solver::pop(uint32_t nscopes) const { NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(d_smtEngine->getOptions().smt.incrementalSolving) + CVC5_API_CHECK(d_smtEngine->getOptions().base.incrementalSolving) << "Cannot pop when not solving incrementally (use --incremental)"; CVC5_API_CHECK(nscopes <= d_smtEngine->getNumUserLevels()) << "Cannot pop beyond first pushed context"; @@ -7176,7 +7177,7 @@ void Solver::push(uint32_t nscopes) const { NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(d_smtEngine->getOptions().smt.incrementalSolving) + CVC5_API_CHECK(d_smtEngine->getOptions().base.incrementalSolving) << "Cannot push when not solving incrementally (use --incremental)"; //////// all checks before this line for (uint32_t n = 0; n < nscopes; ++n) diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 6bdc1abc9..b6ead1b70 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -26,7 +26,8 @@ #include #include "main/main.h" -#include "options/options_public.h" +#include "options/base_options.h" +#include "options/main_options.h" #include "smt/command.h" #include "smt/smt_engine.h" @@ -65,7 +66,7 @@ CommandExecutor::~CommandExecutor() void CommandExecutor::printStatistics(std::ostream& out) const { - if (options::getStatistics(d_options)) + if (d_options.base.statistics) { getSmtEngine()->printStatistics(out); } @@ -73,7 +74,7 @@ void CommandExecutor::printStatistics(std::ostream& out) const void CommandExecutor::printStatisticsSafe(int fd) const { - if (options::getStatistics(d_options)) + if (d_options.base.statistics) { getSmtEngine()->printStatisticsSafe(fd); } @@ -81,7 +82,7 @@ void CommandExecutor::printStatisticsSafe(int fd) const bool CommandExecutor::doCommand(Command* cmd) { - if (options::getParseOnly(d_options)) + if (d_options.base.parseOnly) { return true; } @@ -100,9 +101,9 @@ bool CommandExecutor::doCommand(Command* cmd) return status; } else { - if (options::getVerbosity(d_options) > 2) + if (d_options.base.verbosity > 2) { - *options::getOut(d_options) << "Invoking: " << *cmd << std::endl; + *d_options.base.out << "Invoking: " << *cmd << std::endl; } return doCommandSingleton(cmd); @@ -111,7 +112,7 @@ bool CommandExecutor::doCommand(Command* cmd) void CommandExecutor::reset() { - printStatistics(*options::getErr(d_options)); + printStatistics(*d_options.base.err); /* We have to keep options passed via CL on reset. These options are stored * in CommandExecutor::d_options (populated and created in the driver), and * CommandExecutor::d_options only contains *these* options since the @@ -124,10 +125,10 @@ void CommandExecutor::reset() bool CommandExecutor::doCommandSingleton(Command* cmd) { bool status = true; - if (options::getVerbosity(d_options) >= -1) + if (d_options.base.verbosity >= -1) { status = solverInvoke( - d_solver.get(), d_symman.get(), cmd, options::getOut(d_options)); + d_solver.get(), d_symman.get(), cmd, d_options.base.out); } else { @@ -150,9 +151,9 @@ bool CommandExecutor::doCommandSingleton(Command* cmd) d_result = res = q->getResult(); } - if ((cs != nullptr || q != nullptr) && options::getStatsEveryQuery(d_options)) + if ((cs != nullptr || q != nullptr) && d_options.base.statisticsEveryQuery) { - getSmtEngine()->printStatisticsDiff(*options::getErr(d_options)); + getSmtEngine()->printStatisticsDiff(*d_options.base.err); } bool isResultUnsat = res.isUnsat() || res.isEntailed(); @@ -160,32 +161,32 @@ bool CommandExecutor::doCommandSingleton(Command* cmd) // dump the model/proof/unsat core if option is set if (status) { std::vector > getterCommands; - if (options::getDumpModels(d_options) + if (d_options.driver.dumpModels && (res.isSat() || (res.isSatUnknown() && res.getUnknownExplanation() == api::Result::INCOMPLETE))) { getterCommands.emplace_back(new GetModelCommand()); } - if (options::getDumpProofs(d_options) && isResultUnsat) + if (d_options.driver.dumpProofs && isResultUnsat) { getterCommands.emplace_back(new GetProofCommand()); } - if (options::getDumpInstantiations(d_options) + if (d_options.driver.dumpInstantiations && GetInstantiationsCommand::isEnabled(d_solver.get(), res)) { getterCommands.emplace_back(new GetInstantiationsCommand()); } - if (options::getDumpUnsatCores(d_options) && isResultUnsat) + if ((d_options.driver.dumpUnsatCores || d_options.driver.dumpUnsatCoresFull) && isResultUnsat) { getterCommands.emplace_back(new GetUnsatCoreCommand()); } if (!getterCommands.empty()) { // set no time limit during dumping if applicable - if (options::getForceNoLimitCpuWhileDump(d_options)) + if (d_options.driver.forceNoLimitCpuWhileDump) { setNoLimitCPU(); } @@ -225,17 +226,17 @@ bool solverInvoke(api::Solver* solver, } void CommandExecutor::flushOutputStreams() { - printStatistics(*(options::getErr(d_options))); + printStatistics(*d_options.base.err); // make sure out and err streams are flushed too - if (options::getOut(d_options) != nullptr) + if (d_options.base.out != nullptr) { - *options::getOut(d_options) << std::flush; + *d_options.base.out << std::flush; } - if (options::getErr(d_options) != nullptr) + if (d_options.base.err != nullptr) { - *options::getErr(d_options) << std::flush; + *d_options.base.err << std::flush; } } diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 697501d13..ed1825711 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -33,8 +33,9 @@ #include "main/main.h" #include "main/signal_handlers.h" #include "main/time_limit.h" +#include "options/base_options.h" #include "options/options.h" -#include "options/options_public.h" +#include "options/parser_options.h" #include "options/main_options.h" #include "options/set_language.h" #include "parser/parser.h" @@ -88,9 +89,9 @@ void printUsage(Options& opts, bool full) { << endl << "cvc5 options:" << endl; if(full) { - Options::printUsage(ss.str(), *(options::getOut(opts))); + Options::printUsage(ss.str(), *opts.base.out); } else { - Options::printShortUsage(ss.str(), *(options::getOut(opts))); + Options::printShortUsage(ss.str(), *opts.base.out); } } @@ -116,14 +117,14 @@ int runCvc5(int argc, char* argv[], Options& opts) printUsage(opts, true); exit(1); } - else if (options::getLanguageHelp(opts)) + else if (opts.base.languageHelp) { - Options::printLanguageHelp(*(options::getOut(opts))); + Options::printLanguageHelp(*opts.base.out); exit(1); } else if (opts.driver.version) { - *(options::getOut(opts)) << Configuration::about().c_str() << flush; + *opts.base.out << Configuration::about().c_str() << flush; exit(0); } @@ -131,7 +132,7 @@ int runCvc5(int argc, char* argv[], Options& opts) // If in competition mode, set output stream option to flush immediately #ifdef CVC5_COMPETITION_MODE - *(options::getOut(opts)) << unitbuf; + *opts.base.out << unitbuf; #endif /* CVC5_COMPETITION_MODE */ // We only accept one input file @@ -143,7 +144,7 @@ int runCvc5(int argc, char* argv[], Options& opts) const bool inputFromStdin = filenames.empty() || filenames[0] == "-"; // if we're reading from stdin on a TTY, default to interactive mode - if (!options::wasSetByUserInteractive(opts)) + if (!opts.driver.interactiveWasSetByUser) { opts.driver.interactive = inputFromStdin && isatty(fileno(stdin)); } @@ -157,33 +158,32 @@ int runCvc5(int argc, char* argv[], Options& opts) } const char* filename = filenameStr.c_str(); - if (options::getInputLanguage(opts) == language::input::LANG_AUTO) + if (opts.base.inputLanguage == language::input::LANG_AUTO) { if( inputFromStdin ) { // We can't do any fancy detection on stdin - options::setInputLanguage(language::input::LANG_CVC, opts); + opts.base.inputLanguage = language::input::LANG_CVC; } else { size_t len = filenameStr.size(); if(len >= 5 && !strcmp(".smt2", filename + len - 5)) { - options::setInputLanguage(language::input::LANG_SMTLIB_V2_6, opts); + opts.base.inputLanguage = language::input::LANG_SMTLIB_V2_6; } else if((len >= 2 && !strcmp(".p", filename + len - 2)) || (len >= 5 && !strcmp(".tptp", filename + len - 5))) { - options::setInputLanguage(language::input::LANG_TPTP, opts); + opts.base.inputLanguage = language::input::LANG_TPTP; } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) ) || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) { - options::setInputLanguage(language::input::LANG_CVC, opts); + opts.base.inputLanguage = language::input::LANG_CVC; } else if((len >= 3 && !strcmp(".sy", filename + len - 3)) || (len >= 3 && !strcmp(".sl", filename + len - 3))) { // version 2 sygus is the default - options::setInputLanguage(language::input::LANG_SYGUS_V2, opts); + opts.base.inputLanguage = language::input::LANG_SYGUS_V2; } } } - if (options::getOutputLanguage(opts) == language::output::LANG_AUTO) + if (opts.base.outputLanguage == language::output::LANG_AUTO) { - options::setOutputLanguage( - language::toOutputLanguage(options::getInputLanguage(opts)), opts); + opts.base.outputLanguage = language::toOutputLanguage(opts.base.inputLanguage); } // Determine which messages to show based on smtcomp_mode and verbosity @@ -197,8 +197,8 @@ int runCvc5(int argc, char* argv[], Options& opts) } // important even for muzzled builds (to get result output right) - (*(options::getOut(opts))) - << language::SetLanguage(options::getOutputLanguage(opts)); + (*opts.base.out) + << language::SetLanguage(opts.base.outputLanguage); // Create the command executor to execute the parsed commands pExecutor = std::make_unique(opts); @@ -218,7 +218,7 @@ int runCvc5(int argc, char* argv[], Options& opts) throw Exception( "--tear-down-incremental doesn't work in interactive mode"); } - if (!options::wasSetByUserIncrementalSolving(opts)) + if (!opts.base.incrementalSolvingWasSetByUser) { cmd.reset(new SetOptionCommand("incremental", "true")); cmd->setMuted(true); @@ -245,7 +245,7 @@ int runCvc5(int argc, char* argv[], Options& opts) try { cmd.reset(shell.readCommand()); } catch(UnsafeInterruptException& e) { - (*options::getOut(opts)) << CommandInterrupted(); + *opts.base.out << CommandInterrupted(); break; } if (cmd == nullptr) @@ -258,7 +258,7 @@ int runCvc5(int argc, char* argv[], Options& opts) } else if (opts.driver.tearDownIncremental > 0) { - if (!options::getIncrementalSolving(opts) + if (!opts.base.incrementalSolving && opts.driver.tearDownIncremental > 1) { // For tear-down-incremental values greater than 1, need incremental @@ -266,7 +266,7 @@ int runCvc5(int argc, char* argv[], Options& opts) cmd.reset(new SetOptionCommand("incremental", "true")); cmd->setMuted(true); pExecutor->doCommand(cmd); - // if(options::wasSetByUserIncrementalSolving(opts)) { + // if(opts.base.incrementalWasSetByUser) { // throw OptionException( // "--tear-down-incremental incompatible with --incremental"); // } @@ -282,13 +282,13 @@ int runCvc5(int argc, char* argv[], Options& opts) std::unique_ptr parser(parserBuilder.build()); if( inputFromStdin ) { parser->setInput(Input::newStreamInput( - options::getInputLanguage(opts), cin, filename)); + opts.base.inputLanguage, cin, filename)); } else { - parser->setInput(Input::newFileInput(options::getInputLanguage(opts), + parser->setInput(Input::newFileInput(opts.base.inputLanguage, filename, - options::getMemoryMap(opts))); + opts.parser.memoryMap)); } vector< vector > allCommands; @@ -299,7 +299,7 @@ int runCvc5(int argc, char* argv[], Options& opts) while (status) { if (interrupted) { - (*options::getOut(opts)) << CommandInterrupted(); + *opts.base.out << CommandInterrupted(); break; } @@ -357,7 +357,7 @@ int runCvc5(int argc, char* argv[], Options& opts) } } if (interrupted) continue; - (*options::getOut(opts)) << CommandSuccess(); + *opts.base.out << CommandSuccess(); needReset = 0; } else @@ -436,7 +436,7 @@ int runCvc5(int argc, char* argv[], Options& opts) } else { - if (!options::wasSetByUserIncrementalSolving(opts)) + if (!opts.base.incrementalSolvingWasSetByUser) { cmd.reset(new SetOptionCommand("incremental", "false")); cmd->setMuted(true); @@ -449,20 +449,20 @@ int runCvc5(int argc, char* argv[], Options& opts) std::unique_ptr parser(parserBuilder.build()); if( inputFromStdin ) { parser->setInput(Input::newStreamInput( - options::getInputLanguage(opts), cin, filename)); + opts.base.inputLanguage, cin, filename)); } else { - parser->setInput(Input::newFileInput(options::getInputLanguage(opts), + parser->setInput(Input::newFileInput(opts.base.inputLanguage, filename, - options::getMemoryMap(opts))); + opts.parser.memoryMap)); } bool interrupted = false; while (status) { if (interrupted) { - (*options::getOut(opts)) << CommandInterrupted(); + *opts.base.out << CommandInterrupted(); pExecutor->reset(); break; } @@ -496,9 +496,9 @@ int runCvc5(int argc, char* argv[], Options& opts) } #ifdef CVC5_COMPETITION_MODE - if (cvc5::options::getOut(opts) != nullptr) + if (opts.base.out != nullptr) { - *cvc5::options::getOut(opts) << std::flush; + *opts.base.out << std::flush; } // exit, don't return (don't want destructors to run) // _exit() from unistd.h doesn't run global destructors @@ -510,7 +510,7 @@ int runCvc5(int argc, char* argv[], Options& opts) pExecutor->flushOutputStreams(); #ifdef CVC5_DEBUG - if (opts.driver.earlyExit && options::wasSetByUserEarlyExit(opts)) + if (opts.driver.earlyExit && opts.driver.earlyExitWasSetByUser) { _exit(returnValue); } diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 048c101f0..964b88ea0 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -40,10 +40,11 @@ #include "base/check.h" #include "base/output.h" #include "expr/symbol_manager.h" +#include "options/base_options.h" #include "options/language.h" #include "options/main_options.h" #include "options/options.h" -#include "options/options_public.h" +#include "options/parser_options.h" #include "parser/input.h" #include "parser/parser.h" #include "parser/parser_builder.h" @@ -89,16 +90,16 @@ static set s_declarations; InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm) : d_options(solver->getOptions()), - d_in(*options::getIn(d_options)), - d_out(*options::getOut(d_options)), + d_in(*d_options.base.in), + d_out(*d_options.base.out), d_quit(false) { ParserBuilder parserBuilder(solver, sm, d_options); /* Create parser with bogus input. */ d_parser = parserBuilder.build(); - if (options::wasSetByUserForceLogicString(d_options)) + if (d_options.parser.forceLogicStringWasSetByUser) { - LogicInfo tmp(options::getForceLogicString(d_options)); + LogicInfo tmp(d_options.parser.forceLogicString); d_parser->forceLogic(tmp.getLogicString()); } @@ -113,7 +114,7 @@ InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm) ::using_history(); OutputLanguage lang = - toOutputLanguage(options::getInputLanguage(d_options)); + toOutputLanguage(d_options.base.inputLanguage); switch(lang) { case output::LANG_CVC: d_historyFilename = string(getenv("HOME")) + "/.cvc5_history"; @@ -314,7 +315,7 @@ restart: } d_parser->setInput(Input::newStringInput( - options::getInputLanguage(d_options), input, INPUT_FILENAME)); + d_options.base.inputLanguage, input, INPUT_FILENAME)); /* There may be more than one command in the input. Build up a sequence. */ @@ -365,7 +366,7 @@ restart: } catch (ParserException& pe) { - if (language::isOutputLang_smt2(options::getOutputLanguage(d_options))) + if (language::isOutputLang_smt2(d_options.base.outputLanguage)) { d_out << "(error \"" << pe << "\")" << endl; } diff --git a/src/main/main.cpp b/src/main/main.cpp index 2b25e6c93..a00e29b04 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -26,10 +26,10 @@ #include "base/output.h" #include "main/command_executor.h" #include "main/interactive_shell.h" +#include "options/base_options.h" #include "options/language.h" #include "options/option_exception.h" #include "options/options.h" -#include "options/options_public.h" #include "parser/parser.h" #include "parser/parser_builder.h" #include "parser/parser_exception.h" @@ -53,25 +53,25 @@ int main(int argc, char* argv[]) { return runCvc5(argc, argv, opts); } catch(OptionException& e) { #ifdef CVC5_COMPETITION_MODE - *options::getOut(opts) << "unknown" << endl; + *opts.base.out << "unknown" << endl; #endif cerr << "(error \"" << e << "\")" << endl << endl << "Please use --help to get help on command-line options." << endl; } catch(Exception& e) { #ifdef CVC5_COMPETITION_MODE - *options::getOut(opts) << "unknown" << endl; + *opts.base.out << "unknown" << endl; #endif - if (language::isOutputLang_smt2(options::getOutputLanguage(opts))) + if (language::isOutputLang_smt2(opts.base.outputLanguage)) { - *options::getOut(opts) << "(error \"" << e << "\")" << endl; + *opts.base.out << "(error \"" << e << "\")" << endl; } else { - *options::getErr(opts) << "(error \"" << e << "\")" << endl; + *opts.base.err << "(error \"" << e << "\")" << endl; } - if (options::getStatistics(opts) && pExecutor != nullptr) + if (opts.base.statistics && pExecutor != nullptr) { totalTime.reset(); - pExecutor->printStatistics(*options::getErr(opts)); + pExecutor->printStatistics(*opts.base.err); } } exit(1); diff --git a/src/main/time_limit.cpp b/src/main/time_limit.cpp index c0fc6846a..28a0087bb 100644 --- a/src/main/time_limit.cpp +++ b/src/main/time_limit.cpp @@ -56,7 +56,7 @@ #include #include "base/exception.h" -#include "options/options_public.h" +#include "options/base_options.h" #include "signal_handlers.h" namespace cvc5 { @@ -80,7 +80,7 @@ TimeLimit::~TimeLimit() TimeLimit install_time_limit(const Options& opts) { - unsigned long ms = options::getCumulativeTimeLimit(opts); + uint64_t ms = opts.base.cumulativeMillisecondLimit; // Skip if no time limit shall be set. if (ms == 0) { return TimeLimit(); diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt index 978c32888..26ced1a24 100644 --- a/src/options/CMakeLists.txt +++ b/src/options/CMakeLists.txt @@ -55,7 +55,6 @@ set(options_toml_files proof_options.toml prop_options.toml quantifiers_options.toml - resource_manager_options.toml sep_options.toml sets_options.toml smt_options.toml diff --git a/src/options/base_options.toml b/src/options/base_options.toml index f9d1c1a18..64d373509 100644 --- a/src/options/base_options.toml +++ b/src/options/base_options.toml @@ -1,5 +1,6 @@ id = "BASE" name = "Base" +public = true [[option]] name = "in" @@ -75,6 +76,15 @@ name = "Base" handler = "decreaseVerbosity" help = "decrease verbosity (may be repeated)" +[[option]] + name = "incrementalSolving" + category = "common" + short = "i" + long = "incremental" + type = "bool" + default = "true" + help = "enable incremental solving" + [[option]] name = "statistics" long = "stats" @@ -144,3 +154,52 @@ name = "Base" long = "print-success" type = "bool" help = "print the \"success\" output required of SMT-LIBv2" + +[[option]] + name = "cumulativeMillisecondLimit" + category = "common" + long = "tlimit=MS" + type = "uint64_t" + help = "set time limit in milliseconds of wall clock time" + +[[option]] + name = "perCallMillisecondLimit" + category = "common" + long = "tlimit-per=MS" + type = "uint64_t" + help = "set time limit per query in milliseconds" + +[[option]] + name = "cumulativeResourceLimit" + category = "common" + long = "rlimit=N" + type = "uint64_t" + help = "set resource limit" + +[[option]] + name = "perCallResourceLimit" + alias = ["reproducible-resource-limit"] + category = "common" + long = "rlimit-per=N" + type = "uint64_t" + help = "set resource limit per query" + +# --rweight is used to override the default of one particular resource weight. +# It can be given multiple times to override multiple weights. When options are +# parsed, the resource manager might now be created yet, and it is not clear +# how an option handler would access it in a reasonable way. The option handler +# thus merely puts the data in another option that holds a vector of strings. +# This other option "resourceWeightHolder" has the sole purpose of storing +# this data in a way so that the resource manager can access it in its +# constructor. +[[option]] + category = "expert" + long = "rweight=VAL=N" + type = "std::string" + handler = "setResourceWeight" + help = "set a single resource weight" + +[[option]] + name = "resourceWeightHolder" + category = "undocumented" + type = "std::vector" diff --git a/src/options/main_options.toml b/src/options/main_options.toml index 0f5dfdcd7..fdaebbd6d 100644 --- a/src/options/main_options.toml +++ b/src/options/main_options.toml @@ -95,3 +95,51 @@ public = true type = "int" default = "0" help = "implement PUSH/POP/multi-query by destroying and recreating SmtEngine every N queries" + +[[option]] + name = "dumpModels" + category = "regular" + long = "dump-models" + type = "bool" + default = "false" + help = "output models after every SAT/INVALID/UNKNOWN response" + +[[option]] + name = "dumpProofs" + category = "regular" + long = "dump-proofs" + type = "bool" + default = "false" + help = "output proofs after every UNSAT/VALID response" + +[[option]] + name = "dumpInstantiations" + category = "regular" + long = "dump-instantiations" + type = "bool" + default = "false" + help = "output instantiations of quantified formulas after every UNSAT/VALID response" + +[[option]] + name = "dumpUnsatCores" + category = "regular" + long = "dump-unsat-cores" + type = "bool" + default = "false" + help = "output unsat cores after every UNSAT/VALID response" + +[[option]] + name = "dumpUnsatCoresFull" + category = "regular" + long = "dump-unsat-cores-full" + type = "bool" + default = "false" + help = "dump the full unsat core, including unlabeled assertions" + +[[option]] + name = "forceNoLimitCpuWhileDump" + category = "regular" + long = "force-no-limit-cpu-while-dump" + type = "bool" + default = "false" + help = "Force no CPU limit when dumping models and proofs" diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index c1c843802..1ac5ec56d 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -33,7 +33,6 @@ #include "options/didyoumean.h" #include "options/language.h" #include "options/option_exception.h" -#include "options/resource_manager_options.h" #include "options/smt_options.h" #include "options/theory_options.h" @@ -83,7 +82,7 @@ unsigned long OptionsHandler::limitHandler(std::string option, void OptionsHandler::setResourceWeight(std::string option, std::string optarg) { - d_options->resman.resourceWeightHolder.emplace_back(optarg); + d_options->base.resourceWeightHolder.emplace_back(optarg); } // theory/quantifiers/options_handlers.h diff --git a/src/options/options_public.cpp b/src/options/options_public.cpp index 35e891f5a..552058312 100644 --- a/src/options/options_public.cpp +++ b/src/options/options_public.cpp @@ -17,118 +17,10 @@ #include "options_public.h" -#include -#include -#include -#include - -#include "base/listener.h" -#include "base/modal_exception.h" -#include "options/base_options.h" -#include "options/language.h" -#include "options/main_options.h" -#include "options/option_exception.h" -#include "options/options.h" -#include "options/parser_options.h" -#include "options/printer_modes.h" -#include "options/printer_options.h" -#include "options/resource_manager_options.h" -#include "options/smt_options.h" #include "options/uf_options.h" namespace cvc5::options { -InputLanguage getInputLanguage(const Options& opts) -{ - return opts.base.inputLanguage; -} -InstFormatMode getInstFormatMode(const Options& opts) -{ - return opts.printer.instFormatMode; -} -OutputLanguage getOutputLanguage(const Options& opts) -{ - return opts.base.outputLanguage; -} bool getUfHo(const Options& opts) { return opts.uf.ufHo; } -bool getDumpInstantiations(const Options& opts) -{ - return opts.smt.dumpInstantiations; -} -bool getDumpModels(const Options& opts) { return opts.smt.dumpModels; } -bool getDumpProofs(const Options& opts) { return opts.smt.dumpProofs; } -bool getDumpUnsatCores(const Options& opts) -{ - return opts.smt.dumpUnsatCores || opts.smt.dumpUnsatCoresFull; -} -bool getFilesystemAccess(const Options& opts) -{ - return opts.parser.filesystemAccess; -} -bool getForceNoLimitCpuWhileDump(const Options& opts) -{ - return opts.smt.forceNoLimitCpuWhileDump; -} -bool getIncrementalSolving(const Options& opts) -{ - return opts.smt.incrementalSolving; -} -bool getLanguageHelp(const Options& opts) { return opts.base.languageHelp; } -bool getMemoryMap(const Options& opts) { return opts.parser.memoryMap; } -bool getParseOnly(const Options& opts) { return opts.base.parseOnly; } -bool getProduceModels(const Options& opts) { return opts.smt.produceModels; } -bool getSemanticChecks(const Options& opts) -{ - return opts.parser.semanticChecks; -} -bool getStatistics(const Options& opts) { return opts.base.statistics; } -bool getStatsEveryQuery(const Options& opts) -{ - return opts.base.statisticsEveryQuery; -} -bool getStrictParsing(const Options& opts) -{ - return opts.parser.strictParsing; -} -uint64_t getCumulativeTimeLimit(const Options& opts) -{ - return opts.resman.cumulativeMillisecondLimit; -} -const std::string& getForceLogicString(const Options& opts) -{ - return opts.parser.forceLogicString; -} -int32_t getVerbosity(const Options& opts) { return opts.base.verbosity; } - -std::istream* getIn(const Options& opts) { return opts.base.in; } -std::ostream* getErr(const Options& opts) { return opts.base.err; } -std::ostream* getOut(const Options& opts) { return opts.base.out; } - -void setInputLanguage(InputLanguage val, Options& opts) -{ - opts.base.inputLanguage = val; -} -void setOut(std::ostream* val, Options& opts) { opts.base.out = val; } -void setOutputLanguage(OutputLanguage val, Options& opts) -{ - opts.base.outputLanguage = val; -} - -bool wasSetByUserEarlyExit(const Options& opts) -{ - return opts.driver.earlyExitWasSetByUser; -} -bool wasSetByUserForceLogicString(const Options& opts) -{ - return opts.parser.forceLogicStringWasSetByUser; -} -bool wasSetByUserIncrementalSolving(const Options& opts) -{ - return opts.smt.incrementalSolvingWasSetByUser; -} -bool wasSetByUserInteractive(const Options& opts) -{ - return opts.driver.interactiveWasSetByUser; -} } // namespace cvc5::options diff --git a/src/options/options_public.h b/src/options/options_public.h index 1d2f9edba..60929c96c 100644 --- a/src/options/options_public.h +++ b/src/options/options_public.h @@ -23,47 +23,11 @@ #ifndef CVC5__OPTIONS__OPTIONS_PUBLIC_H #define CVC5__OPTIONS__OPTIONS_PUBLIC_H -#include "options/language.h" #include "options/options.h" -#include "options/printer_modes.h" namespace cvc5::options { -InputLanguage getInputLanguage(const Options& opts) CVC5_EXPORT; -InstFormatMode getInstFormatMode(const Options& opts) CVC5_EXPORT; -OutputLanguage getOutputLanguage(const Options& opts) CVC5_EXPORT; bool getUfHo(const Options& opts) CVC5_EXPORT; -bool getDumpInstantiations(const Options& opts) CVC5_EXPORT; -bool getDumpModels(const Options& opts) CVC5_EXPORT; -bool getDumpProofs(const Options& opts) CVC5_EXPORT; -bool getDumpUnsatCores(const Options& opts) CVC5_EXPORT; -bool getFilesystemAccess(const Options& opts) CVC5_EXPORT; -bool getForceNoLimitCpuWhileDump(const Options& opts) CVC5_EXPORT; -bool getIncrementalSolving(const Options& opts) CVC5_EXPORT; -bool getLanguageHelp(const Options& opts) CVC5_EXPORT; -bool getMemoryMap(const Options& opts) CVC5_EXPORT; -bool getParseOnly(const Options& opts) CVC5_EXPORT; -bool getProduceModels(const Options& opts) CVC5_EXPORT; -bool getSemanticChecks(const Options& opts) CVC5_EXPORT; -bool getStatistics(const Options& opts) CVC5_EXPORT; -bool getStatsEveryQuery(const Options& opts) CVC5_EXPORT; -bool getStrictParsing(const Options& opts) CVC5_EXPORT; -uint64_t getCumulativeTimeLimit(const Options& opts) CVC5_EXPORT; -const std::string& getForceLogicString(const Options& opts) CVC5_EXPORT; -int32_t getVerbosity(const Options& opts) CVC5_EXPORT; - -std::istream* getIn(const Options& opts) CVC5_EXPORT; -std::ostream* getErr(const Options& opts) CVC5_EXPORT; -std::ostream* getOut(const Options& opts) CVC5_EXPORT; - -void setInputLanguage(InputLanguage val, Options& opts) CVC5_EXPORT; -void setOut(std::ostream* val, Options& opts) CVC5_EXPORT; -void setOutputLanguage(OutputLanguage val, Options& opts) CVC5_EXPORT; - -bool wasSetByUserEarlyExit(const Options& opts) CVC5_EXPORT; -bool wasSetByUserForceLogicString(const Options& opts) CVC5_EXPORT; -bool wasSetByUserIncrementalSolving(const Options& opts) CVC5_EXPORT; -bool wasSetByUserInteractive(const Options& opts) CVC5_EXPORT; } // namespace cvc5::options diff --git a/src/options/parser_options.toml b/src/options/parser_options.toml index 6fc683368..f19b903a6 100644 --- a/src/options/parser_options.toml +++ b/src/options/parser_options.toml @@ -1,5 +1,6 @@ id = "PARSER" name = "Parser" +public = true [[option]] name = "strictParsing" diff --git a/src/options/resource_manager_options.toml b/src/options/resource_manager_options.toml deleted file mode 100644 index 6d5c4d4cf..000000000 --- a/src/options/resource_manager_options.toml +++ /dev/null @@ -1,51 +0,0 @@ -id = "RESMAN" -name = "Resource Manager" - -[[option]] - name = "cumulativeMillisecondLimit" - category = "common" - long = "tlimit=MS" - type = "uint64_t" - help = "set time limit in milliseconds of wall clock time" - -[[option]] - name = "perCallMillisecondLimit" - category = "common" - long = "tlimit-per=MS" - type = "uint64_t" - help = "set time limit per query in milliseconds" - -[[option]] - name = "cumulativeResourceLimit" - category = "common" - long = "rlimit=N" - type = "uint64_t" - help = "set resource limit" - -[[option]] - name = "perCallResourceLimit" - alias = ["reproducible-resource-limit"] - category = "common" - long = "rlimit-per=N" - type = "uint64_t" - help = "set resource limit per query" - -# --rweight is used to override the default of one particular resource weight. -# It can be given multiple times to override multiple weights. When options are -# parsed, the resource manager might now be created yet, and it is not clear -# how an option handler would access it in a reasonable way. The option handler -# thus merely puts the data in another option that holds a vector of strings. -# This other option "resourceWeightHolder" has the sole purpose of storing -# this data in a way so that the resource manager can access it in its -# constructor. -[[option]] - category = "expert" - long = "rweight=VAL=N" - type = "std::string" - handler = "setResourceWeight" - help = "set a single resource weight" - -[[option]] - name = "resourceWeightHolder" - category = "undocumented" - type = "std::vector" diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index d1354f777..4d08aa672 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -78,14 +78,6 @@ name = "SMT Layer" type = "bool" help = "after SAT/INVALID/UNKNOWN, check that the generated model satisfies user and internal assertions" -[[option]] - name = "dumpModels" - category = "regular" - long = "dump-models" - type = "bool" - default = "false" - help = "output models after every SAT/INVALID/UNKNOWN response" - [[option]] name = "modelCoresMode" category = "regular" @@ -130,14 +122,6 @@ name = "SMT Layer" default = "false" help = "produce proofs, support check-proofs and get-proof" -[[option]] - name = "dumpProofs" - category = "regular" - long = "dump-proofs" - type = "bool" - default = "false" - help = "output proofs after every UNSAT/VALID response" - [[option]] name = "checkProofs" category = "regular" @@ -145,14 +129,6 @@ name = "SMT Layer" type = "bool" help = "after UNSAT/VALID, check the generated proof (with proof)" -[[option]] - name = "dumpInstantiations" - category = "regular" - long = "dump-instantiations" - type = "bool" - default = "false" - help = "output instantiations of quantified formulas after every UNSAT/VALID response" - [[option]] name = "sygusOut" category = "regular" @@ -217,22 +193,6 @@ name = "SMT Layer" type = "bool" help = "after UNSAT/VALID, produce and check an unsat core (expensive)" -[[option]] - name = "dumpUnsatCores" - category = "regular" - long = "dump-unsat-cores" - type = "bool" - default = "false" - help = "output unsat cores after every UNSAT/VALID response" - -[[option]] - name = "dumpUnsatCoresFull" - category = "regular" - long = "dump-unsat-cores-full" - type = "bool" - default = "false" - help = "dump the full unsat core, including unlabeled assertions" - [[option]] name = "unsatAssumptions" category = "regular" @@ -359,15 +319,6 @@ name = "SMT Layer" default = "false" help = "calculate sort inference of input problem, convert the input based on monotonic sorts" -[[option]] - name = "incrementalSolving" - category = "common" - short = "i" - long = "incremental" - type = "bool" - default = "true" - help = "enable incremental solving" - [[option]] name = "abstractValues" category = "regular" @@ -421,14 +372,6 @@ name = "SMT Layer" type = "std::string" help = "set the diagnostic output channel of the solver" -[[option]] - name = "forceNoLimitCpuWhileDump" - category = "regular" - long = "force-no-limit-cpu-while-dump" - type = "bool" - default = "false" - help = "Force no CPU limit when dumping models and proofs" - [[option]] name = "foreignTheoryRewrite" category = "regular" diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index d96e94d43..eab982013 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -26,8 +26,8 @@ #include "base/check.h" #include "base/output.h" #include "expr/kind.h" +#include "options/base_options.h" #include "options/options.h" -#include "options/options_public.h" #include "parser/input.h" #include "parser/parser_exception.h" #include "smt/command.h" @@ -900,7 +900,7 @@ std::wstring Parser::processAdHocStringEsc(const std::string& s) api::Term Parser::mkStringConstant(const std::string& s) { if (language::isInputLang_smt2_6( - options::getInputLanguage(d_solver->getOptions()))) + d_solver->getOptions().base.inputLanguage)) { return d_solver->mkString(s, true); } diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index 1f25e00dd..816803ccc 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -21,8 +21,9 @@ #include "api/cpp/cvc5.h" #include "base/check.h" #include "cvc/cvc.h" +#include "options/base_options.h" #include "options/options.h" -#include "options/options_public.h" +#include "options/parser_options.h" #include "parser/antlr_input.h" #include "parser/input.h" #include "parser/parser.h" @@ -120,14 +121,14 @@ ParserBuilder& ParserBuilder::withParseOnly(bool flag) { ParserBuilder& ParserBuilder::withOptions(const Options& opts) { ParserBuilder& retval = *this; - retval = retval.withInputLanguage(options::getInputLanguage(opts)) - .withChecks(options::getSemanticChecks(opts)) - .withStrictMode(options::getStrictParsing(opts)) - .withParseOnly(options::getParseOnly(opts)) - .withIncludeFile(options::getFilesystemAccess(opts)); - if (options::wasSetByUserForceLogicString(opts)) + retval = retval.withInputLanguage(opts.base.inputLanguage) + .withChecks(opts.parser.semanticChecks) + .withStrictMode(opts.parser.strictParsing) + .withParseOnly(opts.base.parseOnly) + .withIncludeFile(opts.parser.filesystemAccess); + if (opts.parser.forceLogicStringWasSetByUser) { - LogicInfo tmp(options::getForceLogicString(opts)); + LogicInfo tmp(opts.parser.forceLogicString); retval = retval.withForcedLogic(tmp.getLogicString()); } return retval; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 56aebdcf7..282b72974 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -17,6 +17,7 @@ #include #include "base/check.h" +#include "options/base_options.h" #include "options/options.h" #include "options/options_public.h" #include "parser/antlr_input.h" @@ -846,7 +847,7 @@ api::Term Smt2::mkAbstractValue(const std::string& name) InputLanguage Smt2::getLanguage() const { - return options::getInputLanguage(d_solver->getOptions()); + return d_solver->getOptions().base.inputLanguage; } void Smt2::parseOpApplyTypeAscription(ParseOp& p, api::Sort type) diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp index 89029b5eb..eb6410291 100644 --- a/src/preprocessing/passes/ackermann.cpp +++ b/src/preprocessing/passes/ackermann.cpp @@ -29,8 +29,8 @@ #include "base/check.h" #include "expr/node_algorithm.h" #include "expr/skolem_manager.h" +#include "options/base_options.h" #include "options/options.h" -#include "options/smt_options.h" #include "preprocessing/assertion_pipeline.h" #include "preprocessing/preprocessing_pass_context.h" diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp index 15a16888d..df9d44e39 100644 --- a/src/preprocessing/passes/int_to_bv.cpp +++ b/src/preprocessing/passes/int_to_bv.cpp @@ -26,6 +26,7 @@ #include "expr/node.h" #include "expr/node_traversal.h" #include "expr/skolem_manager.h" +#include "options/base_options.h" #include "options/smt_options.h" #include "preprocessing/assertion_pipeline.h" #include "theory/rewriter.h" diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp index 5bfb2a79f..d1dd389ae 100644 --- a/src/preprocessing/passes/ite_simp.cpp +++ b/src/preprocessing/passes/ite_simp.cpp @@ -17,6 +17,7 @@ #include +#include "options/base_options.h" #include "options/smt_options.h" #include "preprocessing/assertion_pipeline.h" #include "preprocessing/preprocessing_pass_context.h" diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index 79fcc4028..a5720e758 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -22,7 +22,7 @@ #include "expr/node_self_iterator.h" #include "expr/skolem_manager.h" #include "options/arith_options.h" -#include "options/smt_options.h" +#include "options/base_options.h" #include "preprocessing/assertion_pipeline.h" #include "preprocessing/preprocessing_pass_context.h" #include "smt/smt_statistics_registry.h" diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index fd86d3a42..6f99a47f0 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -27,6 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "base/check.h" #include "base/output.h" +#include "options/base_options.h" #include "options/main_options.h" #include "options/prop_options.h" #include "options/smt_options.h" diff --git a/src/smt/command.cpp b/src/smt/command.cpp index d672b79a6..5f0da7a0c 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -31,6 +31,7 @@ #include "expr/symbol_manager.h" #include "expr/type_node.h" #include "options/options.h" +#include "options/main_options.h" #include "options/printer_options.h" #include "options/smt_options.h" #include "printer/printer.h" diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp index 7406b922e..3c0a4ac5b 100644 --- a/src/smt/preprocessor.cpp +++ b/src/smt/preprocessor.cpp @@ -15,6 +15,7 @@ #include "smt/preprocessor.h" +#include "options/base_options.h" #include "options/expr_options.h" #include "options/smt_options.h" #include "preprocessing/preprocessing_pass_context.h" diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index cd05b84c4..e119ce4d4 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -66,7 +66,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // unsat cores and proofs shenanigans if (options::dumpUnsatCoresFull()) { - opts.smt.dumpUnsatCores = true; + opts.driver.dumpUnsatCores = true; } if (options::checkUnsatCores() || options::dumpUnsatCores() || options::unsatAssumptions() diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index bd48fe0ea..9056e7c94 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -29,7 +29,6 @@ #include "options/option_exception.h" #include "options/printer_options.h" #include "options/proof_options.h" -#include "options/resource_manager_options.h" #include "options/smt_options.h" #include "options/theory_options.h" #include "printer/printer.h" @@ -1811,16 +1810,16 @@ void SmtEngine::setResourceLimit(uint64_t units, bool cumulative) { if (cumulative) { - d_env->d_options.resman.cumulativeResourceLimit = units; + d_env->d_options.base.cumulativeResourceLimit = units; } else { - d_env->d_options.resman.perCallResourceLimit = units; + d_env->d_options.base.perCallResourceLimit = units; } } void SmtEngine::setTimeLimit(uint64_t millis) { - d_env->d_options.resman.perCallMillisecondLimit = millis; + d_env->d_options.base.perCallMillisecondLimit = millis; } unsigned long SmtEngine::getResourceUsage() const diff --git a/src/smt/smt_engine_state.cpp b/src/smt/smt_engine_state.cpp index 4afa15a3b..cb0a94123 100644 --- a/src/smt/smt_engine_state.cpp +++ b/src/smt/smt_engine_state.cpp @@ -16,6 +16,7 @@ #include "smt/smt_engine_state.h" #include "base/modal_exception.h" +#include "options/base_options.h" #include "options/option_exception.h" #include "options/smt_options.h" #include "smt/smt_engine.h" diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp index 8fa610cda..98278ef9e 100644 --- a/src/smt/sygus_solver.cpp +++ b/src/smt/sygus_solver.cpp @@ -20,6 +20,7 @@ #include "base/modal_exception.h" #include "expr/dtype.h" #include "expr/skolem_manager.h" +#include "options/base_options.h" #include "options/option_exception.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp index 99b95719f..3dff64113 100644 --- a/src/theory/arith/arith_ite_utils.cpp +++ b/src/theory/arith/arith_ite_utils.cpp @@ -22,6 +22,7 @@ #include "base/output.h" #include "expr/skolem_manager.h" +#include "options/base_options.h" #include "options/smt_options.h" #include "preprocessing/util/ite_utilities.h" #include "theory/arith/arith_utilities.h" diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index a675c1bf4..97b29b6b3 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -35,7 +35,7 @@ #include "expr/node_builder.h" #include "expr/skolem_manager.h" #include "options/arith_options.h" -#include "options/smt_options.h" // for incrementalSolving() +#include "options/base_options.h" #include "preprocessing/util/ite_utilities.h" #include "proof/proof_generator.h" #include "proof/proof_node_manager.h" diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp index 9871f2a92..55ed6c41d 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.cpp +++ b/src/theory/bv/bitblast/eager_bitblaster.cpp @@ -16,6 +16,7 @@ #include "theory/bv/bitblast/eager_bitblaster.h" #include "cvc5_private.h" +#include "options/base_options.h" #include "options/bv_options.h" #include "options/smt_options.h" #include "prop/cnf_stream.h" diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp index 2d0ae1931..b0082b992 100644 --- a/src/theory/bv/bv_eager_solver.cpp +++ b/src/theory/bv/bv_eager_solver.cpp @@ -15,6 +15,7 @@ #include "theory/bv/bv_eager_solver.h" +#include "options/base_options.h" #include "options/bv_options.h" #include "options/smt_options.h" #include "theory/bv/bitblast/aig_bitblaster.h" diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 71f4028ec..0f82d8301 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -16,6 +16,7 @@ #include "theory/quantifiers/instantiate.h" #include "expr/node_algorithm.h" +#include "options/base_options.h" #include "options/printer_options.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp index 5b7bd1552..31e5240df 100644 --- a/src/theory/quantifiers/term_registry.cpp +++ b/src/theory/quantifiers/term_registry.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/term_registry.h" +#include "options/base_options.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" #include "theory/quantifiers/first_order_model.h" diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp index f0cc78789..c4a94dfa2 100644 --- a/src/util/resource_manager.cpp +++ b/src/util/resource_manager.cpp @@ -22,9 +22,9 @@ #include "base/check.h" #include "base/listener.h" #include "base/output.h" +#include "options/base_options.h" #include "options/option_exception.h" #include "options/options.h" -#include "options/resource_manager_options.h" #include "util/statistics_registry.h" using namespace std; @@ -164,7 +164,7 @@ ResourceManager::ResourceManager(StatisticsRegistry& stats, d_infidWeights.fill(1); d_resourceWeights.fill(1); - for (const auto& opt : d_options.resman.resourceWeightHolder) + for (const auto& opt : d_options.base.resourceWeightHolder) { std::string name; uint64_t weight; @@ -189,9 +189,9 @@ uint64_t ResourceManager::getTimeUsage() const { return d_cumulativeTimeUsed; } uint64_t ResourceManager::getResourceRemaining() const { - if (d_options.resman.cumulativeResourceLimit <= d_cumulativeResourceUsed) + if (d_options.base.cumulativeResourceLimit <= d_cumulativeResourceUsed) return 0; - return d_options.resman.cumulativeResourceLimit - d_cumulativeResourceUsed; + return d_options.base.cumulativeResourceLimit - d_cumulativeResourceUsed; } void ResourceManager::spendResource(uint64_t amount) @@ -237,21 +237,21 @@ void ResourceManager::spendResource(theory::InferenceId iid) void ResourceManager::beginCall() { - d_perCallTimer.set(d_options.resman.perCallMillisecondLimit); + d_perCallTimer.set(d_options.base.perCallMillisecondLimit); d_thisCallResourceUsed = 0; - if (d_options.resman.cumulativeResourceLimit > 0) + if (d_options.base.cumulativeResourceLimit > 0) { // Compute remaining cumulative resource budget d_thisCallResourceBudget = - d_options.resman.cumulativeResourceLimit - d_cumulativeResourceUsed; + d_options.base.cumulativeResourceLimit - d_cumulativeResourceUsed; } - if (d_options.resman.perCallResourceLimit > 0) + if (d_options.base.perCallResourceLimit > 0) { // Check if per-call resource budget is even smaller - if (d_options.resman.perCallResourceLimit < d_thisCallResourceBudget) + if (d_options.base.perCallResourceLimit < d_thisCallResourceBudget) { - d_thisCallResourceBudget = d_options.resman.perCallResourceLimit; + d_thisCallResourceBudget = d_options.base.perCallResourceLimit; } } } @@ -265,25 +265,25 @@ void ResourceManager::endCall() bool ResourceManager::limitOn() const { - return (d_options.resman.cumulativeResourceLimit > 0) - || (d_options.resman.perCallMillisecondLimit > 0) - || (d_options.resman.perCallResourceLimit > 0); + return (d_options.base.cumulativeResourceLimit > 0) + || (d_options.base.perCallMillisecondLimit > 0) + || (d_options.base.perCallResourceLimit > 0); } bool ResourceManager::outOfResources() const { - if (d_options.resman.perCallResourceLimit > 0) + if (d_options.base.perCallResourceLimit > 0) { // Check if per-call resources are exhausted - if (d_thisCallResourceUsed >= d_options.resman.perCallResourceLimit) + if (d_thisCallResourceUsed >= d_options.base.perCallResourceLimit) { return true; } } - if (d_options.resman.cumulativeResourceLimit > 0) + if (d_options.base.cumulativeResourceLimit > 0) { // Check if cumulative resources are exhausted - if (d_cumulativeResourceUsed >= d_options.resman.cumulativeResourceLimit) + if (d_cumulativeResourceUsed >= d_options.base.cumulativeResourceLimit) { return true; } @@ -293,7 +293,7 @@ bool ResourceManager::outOfResources() const bool ResourceManager::outOfTime() const { - if (d_options.resman.perCallMillisecondLimit == 0) return false; + if (d_options.base.perCallMillisecondLimit == 0) return false; return d_perCallTimer.expired(); } diff --git a/test/api/smt2_compliance.cpp b/test/api/smt2_compliance.cpp index 9794888b2..ee58b7ad4 100644 --- a/test/api/smt2_compliance.cpp +++ b/test/api/smt2_compliance.cpp @@ -18,6 +18,7 @@ #include #include "api/cpp/cvc5.h" +#include "options/base_options.h" #include "options/options.h" #include "options/options_public.h" #include "options/set_language.h" @@ -35,8 +36,8 @@ void testGetInfo(api::Solver* solver, const char* s); int main() { Options opts; - options::setInputLanguage(language::input::LANG_SMTLIB_V2, opts); - options::setOutputLanguage(language::output::LANG_SMTLIB_V2, opts); + opts.base.inputLanguage = language::input::LANG_SMTLIB_V2; + opts.base.outputLanguage = language::output::LANG_SMTLIB_V2; cout << language::SetLanguage(language::output::LANG_SMTLIB_V2); -- cgit v1.2.3 From 44299210154706701d56bfa40e8cb5c58079e9ca Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 15 Jun 2021 23:00:47 +0200 Subject: Add cocoalib (#6731) This PR adds CoCoALib as an optional dependency. It will be used in the CAD-based nonlinear solver for computer algebra routines beyond the capabilities of libpoly like quotient rings and polynomial factorization. --- CMakeLists.txt | 7 ++++ cmake/FindCoCoA.cmake | 96 +++++++++++++++++++++++++++++++++++++++++++++++++++ configure.sh | 7 ++++ 3 files changed, 110 insertions(+) create mode 100644 cmake/FindCoCoA.cmake diff --git a/CMakeLists.txt b/CMakeLists.txt index d7512e874..b555c7bdc 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -127,6 +127,7 @@ cvc5_option(USE_EDITLINE "Use Editline for better interactive support") # >> 2-valued: ON OFF # > for options where we don't need to detect if set by user (default: OFF) option(USE_POLY "Use LibPoly for polynomial arithmetic") +option(USE_COCOA "Use CoCoALib for further polynomial operations") option(USE_SYMFPU "Use SymFPU for floating point support") option(USE_PYTHON2 "Force Python 2 (deprecated)") @@ -462,6 +463,11 @@ else() set(CVC5_USE_POLY_IMP 0) endif() +if(USE_COCOA) + find_package(CoCoA REQUIRED 0.99711) + add_definitions(-DCVC5_USE_COCOA) +endif() + if(USE_EDITLINE) find_package(Editline REQUIRED) set(HAVE_LIBEDITLINE 1) @@ -657,6 +663,7 @@ print_config("CryptoMiniSat " ${USE_CRYPTOMINISAT}) print_config("GLPK " ${USE_GLPK}) print_config("Kissat " ${USE_KISSAT}) print_config("LibPoly " ${USE_POLY}) +print_config("CoCoALib " ${USE_COCOA}) message("") print_config("Build libcvc5 only " ${BUILD_LIB_ONLY}) diff --git a/cmake/FindCoCoA.cmake b/cmake/FindCoCoA.cmake new file mode 100644 index 000000000..1a4f82e9f --- /dev/null +++ b/cmake/FindCoCoA.cmake @@ -0,0 +1,96 @@ +############################################################################### +# Top contributors (to current version): +# Gereon Kremer +# +# 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. +# ############################################################################# +# +# Find CoCoA +# CoCoA_FOUND - system has CoCoA lib +# CoCoA_INCLUDE_DIR - the CoCoA include directory +# CoCoA_LIBRARIES - Libraries needed to use CoCoA +## + +include(deps-helper) + +find_path(CoCoA_INCLUDE_DIR NAMES CoCoA/CoCoA.h) +find_library(CoCoA_LIBRARIES NAMES CoCoA) + +set(CoCoA_FOUND_SYSTEM FALSE) +if(CoCoA_INCLUDE_DIR AND CoCoA_LIBRARIES) + set(CoCoA_FOUND_SYSTEM TRUE) + + file(STRINGS ${CoCoA_INCLUDE_DIR}/CoCoA/library.H CoCoA_VERSION + REGEX "^COCOALIB_VERSION=.*" + ) + string(REGEX MATCH "[0-9]+\\.[0-9]+" CoCoA_VERSION "${CoCoA_VERSION}") + + check_system_version("CoCoA") +endif() + +if(NOT CoCoA_FOUND_SYSTEM) + check_ep_downloaded("CoCoA-EP") + if(NOT CoCoA-EP_DOWNLOADED) + check_auto_download("CoCoA" "--no-cocoa") + endif() + + include(ExternalProject) + + set(CoCoA_VERSION "0.99712") + + if("${CMAKE_GENERATOR}" STREQUAL "Unix Makefiles") + # use $(MAKE) instead of "make" to allow for parallel builds + set(make_cmd "$(MAKE)") + else() + # $(MAKE) does not work with ninja + set(make_cmd "make") + endif() + + ExternalProject_Add( + CoCoA-EP + ${COMMON_EP_CONFIG} + URL "http://cocoa.dima.unige.it/cocoalib/tgz/CoCoALib-${CoCoA_VERSION}.tgz" + URL_HASH SHA1=873d0b60800cd3852939816ce0aa2e7f72dac4ce + BUILD_IN_SOURCE YES + CONFIGURE_COMMAND ./configure --prefix= + BUILD_COMMAND ${make_cmd} library + ) + # Remove install directory before make install. CoCoA will complain otherwise + ExternalProject_Add_Step( + CoCoA-EP clear-install + COMMAND ${CMAKE_COMMAND} -E remove_directory /include/CoCoA-${CoCoA_VERSION} + DEPENDEES build + DEPENDERS install + ) + + add_dependencies(CoCoA-EP GMP) + + set(CoCoA_INCLUDE_DIR "${DEPS_BASE}/include/") + set(CoCoA_LIBRARIES "${DEPS_BASE}/lib/libcocoa.a") +endif() + +set(CoCoA_FOUND TRUE) + +add_library(CoCoA STATIC IMPORTED GLOBAL) +set_target_properties(CoCoA PROPERTIES IMPORTED_LOCATION "${CoCoA_LIBRARIES}") +set_target_properties( + CoCoA PROPERTIES INTERFACE_INCLUDE_DIRECTORIES "${CoCoA_INCLUDE_DIR}" +) +set_target_properties(CoCoA PROPERTIES INTERFACE_LINK_LIBRARIES GMP) + +mark_as_advanced(CoCoA_FOUND) +mark_as_advanced(CoCoA_FOUND_SYSTEM) +mark_as_advanced(CoCoA_INCLUDE_DIR) +mark_as_advanced(CoCoA_LIBRARIES) + +if(CoCoA_FOUND_SYSTEM) + message(STATUS "Found CoCoA ${CoCoA_VERSION}: ${CoCoA_LIBRARIES}") +else() + message(STATUS "Building CoCoA ${CoCoA_VERSION}: ${CoCoA_LIBRARIES}") + add_dependencies(CoCoA CoCoA-EP) +endif() diff --git a/configure.sh b/configure.sh index 3e59cadc9..487bbcb5a 100755 --- a/configure.sh +++ b/configure.sh @@ -63,6 +63,7 @@ The following flags enable optional packages (disable with --no-