summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-07-01Add testing infrastructure for LFSC signatures (#4678)Andres Noetzli
This commit adds testing infrastructure for LFSC signatures that is enabled when CVC4 is configured with LFSC. The testing infrastructure adopts run_test.py from https://github.com/CVC4/LFSC with minor modifications (mainly adding support for a list of include directories that are searched to resolve *.plf dependencies). The commit uses the existing examples and test files from proofs/signatures as the initial set of tests. Co-authored-by: Alex Ozdemir aozdemir@hmc.edu
2020-07-01 Inferences and model construction taking into account seq.unit (#4607)Andrew Reynolds
Towards theory of sequences. This makes the strings solver handle seq.unit, which requires two new inferences and updates to its model construction. It also fixes a bug in the best content heuristic, which previously failed to update the best score.
2020-07-01(proof-new) Updates to evaluator (#4659)Andrew Reynolds
This will be required to separate "evaluation steps" from "rewrite steps" when reconstructing proofs of rewrites.
2020-06-30(proof-new) Improve rewriter for WITNESS (#4661)Andrew Reynolds
Proof checking failures revealed that we are not rewriting witness for Boolean variables (witness ((x Bool)) x) ---> true and (witness ((x Bool)) (not x)) ---> false. Also adds 2 assertions that are required for elimination (witness ((x T)) (= x t)) ---> t. These assertions should always hold due to the witness terms we construct.
2020-06-30Fix normal form for re.comp (#4676)Andrew Reynolds
Fixes #4674.
2020-06-30Update NEWS post 1.8 release (#4666)Andres Noetzli
2020-06-30Fix GMP compilation for win64. (#4675)Mathias Preiner
2020-06-30Simplify quantifiers strategy for when to apply last call effort check with ↵Andrew Reynolds
fmfBound (#4673) There was a strategy in place for alternating which rounds quantifier instantiation would run on when --fmf-bound is enabled. However, this made it so that in some cases, no instantiation strategy would be applied, if e.g. fmfBound was enabled but no quantified formulas were handled by that strategy. It is not clear if this strategy is a good idea, considering all use cases of quantifiers, and hence this PR deletes this block of code. This makes it so that several eqrange benchmarks are answered "unsat" quickly.
2020-06-30Interpolation step 1 (#4638)Ying Sheng
This is the first step of adding Interpolation. The whole change will be adding the API for (get-interpol s B), which is aim for computes an I that A->I and I->B. Here A is the assertions in the stack. The first step creates the API framework, while omits the implementation for getting interpolation.
2020-06-30contrib: Update to GMP 6.2.0, compile static and shared libraries. (#4671)Mathias Preiner
2020-06-29Add internal support for integer and operator (#4668)Andrew Reynolds
Towards merging iand branch to master. This adds internal support for an "integer AND" operator.
2020-06-29Make ExprManager constructor private (#4669)Andres Noetzli
This commit makes the ExprManager constructor private and updates the initialization of subsolvers, unit tests, and system tests accordingly. This is a step towards making options part of SmtEngine instead of NodeManager.
2020-06-29Python Sort tests (#4639)makaimann
This commit ports over the sort_black tests to the pytest infrastructure to test the Python bindings. It also adds missing functionality that was revealed during the testing.
2020-06-29Fix memory leak in unit test node_algorithm_black (#4670)Andres Noetzli
Commit ccd4500 modified the unit test node_algorithm_black. It added d_bvTypeNode as a data member to the class and initialized it in setUp() but did not free it in tearDown(), which set off ASan. This commit fixes tearDown() to free d_bvTypeNode. Marking this as major because it should fix the nightlies.
2020-06-28Fix non-termination issues in simpleRegExpConsume (#4667)Andrew Reynolds
There were two issues related to RE in bodies of re.* that accepted the empty string that led to non-termination in the rewriter for regular expressions. This also improves trace messages for simpleRegExpConsume. Fixes #4662.
2020-06-28Proof Rules and Checker for Arithmetic (#4665)Alex Ozdemir
This PR introduces proof rules for arithmetic and their checker. The code is dead, since these rules are never used.
2020-06-27Add API for retrieving separation heap/nil term (#4663)Andres Noetzli
This commit extends the API to support the retrieval of heap/nil term when separation logic is used and changes the corresponding system test accordingly. This commit is in preparation of making the constructor of `ExprManager` private.
2020-06-25fix and test (#4658)yoni206
This PR adds support for indexed operators (such as extract) to getOperatorsMap in node_algorithm.cpp. The corresponding test is augmented accordingly.
2020-06-25(proof-new) Add TrustNode interfaces to OutputChannel (#4643)Andrew Reynolds
2020-06-25Remove sygus1 parser (#4651)Andrew Reynolds
We no longer support sygus v1 inputs. This PR removes support for sygus v1 (as well as a deprecated "z3str" variant of smt lib 2 which is subsumed by the new strings standard). As mentioned in the release notes, CVC4 1.8 supports a conversion from sygus v1 to v2 script. This removal is required for further updates to the new API. Further infrastructure (e.g. the sygus print callback) will be removed in a separate PR. FYI @abdoo8080 .
2020-06-25Update option --nl-ext to enable/disable incremental linearization solver ↵Andrew Reynolds
only (#4649) Previously, this option disabled/enabled the entire non-linear solver. This is in preparation for new CAD techniques. I am intentionally not renaming "--nl-ext" to e.g. "--nl-inc-lin" for the sake of not breaking user configurations. It makes some minor changes to clean the interface in a few places and to not enable the non-linear solver in linear logics.
2020-06-24Fix CVC4_EXTRAVERSION variable (#4653)Andres Noetzli
When I created the PR for 733083c, it did not contain the change from "" -> "-prerelease" because at the time master still had CVC4_EXTRAVERSION set to "-prerelease". This commit fixes CVC4_EXTRAVERSION.
2020-06-24[unconstrained] Fix gathering of visited-once vars (#4652)Andres Noetzli
Fixes #4644. This commit fixes an issue where the set `d_unconstrained` in the unconstrained simplification pass was not computed correctly. The problem was that visiting the same term multiple times did not remove the variables appearing in that term from the visited-once set. A simple example that triggers the issue is the following: ``` (set-logic ALL) (declare-fun a () Bool) (declare-fun b () Bool) (assert (not (= a b))) (assert (= a (= a b))) (check-sat) ``` After running `UnconstrainedSimplifier::visitAll()` on both assertions, we end up with `[b]` as our `d_unconstrained` set. We end up inferring the substitution `(= a b) --> b` and get `(not b)` and `b`, which is unsat even though the original problem is sat. This commit fixes the issue by visiting all the children of a node if we visit a node for a second time. This makes sure that we remove any children from the visisted-once set.
2020-06-23(proof-new) Updates to proof node manager (#4617)Andrew Reynolds
Main feature added is the mkScope interface, which is agnostic to symmetry of (dis)equalities. It also adds a check for cyclic proofs when using the interface ProofNodeManager::updateNode. Note that an earlier version of this method was agnostics to predicates vs Boolean equality with constants. This is no longer required.
2020-06-23New C++ API: Remove examples for old API. (#4650)Aina Niemetz
This removes obsolete examples for the old API in preparation of making the old API private. Examples for the new API are renamed from *-new.cpp to *.cpp.
2020-06-23Add support for eqrange predicate (#4562)Mathias Preiner
This commit adds support for an eqrange predicate. (eqrange a b i j) is true if arrays a and b are equal on all indices within indices i and j, i.e., \forall k . i <= k <= j --> a[k] = b[k]. Requires option --arrays-exp to be enabled.
2020-06-22(proof-new) Add REWRITE trust node kind. (#4624)Andrew Reynolds
This will be used for a number of purposes, including tracking proofs for rewriting and preprocessing.
2020-06-22get-authors: Add alias for nafur. (#4646)Aina Niemetz
2020-06-22Allow for better interaction of Integer/Rational with mpz_class/mpq_class. ↵nafur
(#4612)
2020-06-22(proof-new) Add proof-new to options file (#4641)Andrew Reynolds
Adds proof-new as an option. This is required for adding code that is guarded by this option while we are in the process of merging work on the new proofs infrastructure. Enabling the option currently throws an option exception.
2020-06-22Add trascendental function kinds to list of unevaluated operators (#4640)Andrew Reynolds
Fixes #4636. This adds transcendental function kinds to the list of unevaluated operators (operators that don't necessarily rewrite to constants when applied to constant children). One consequence of this is that when models are enabled, we cannot solve for equations like (= a (cos b)), since the value of (cos b) is not necessarily evaluable, and hence must be approximated. As a result, we answer the benchmark on #4636 instead of generating an incorrect model (when models are enabled). When models are disabled, we answer "sat". A regression had a similar issue which happened to be succeeding. I've added --no-check-models to this regression (or otherwise we would answer unknown for this benchmark).
2020-06-22fix (#4637)yoni206
The help message of --bv-print-consts-as-indexed-symbols seems wrong to me, and this PR suggests a fix.
2020-06-19Use traversal iterators in IntToBv (#4169)Alex Ozdemir
This commit rips the traversal machinery out of Int-to-Bv, replacing it with traversal iterators. Also, cleaned `childrenTypesChanged` a bit. While basically I just cut out some lines, the diff is rather messy (I think the diffing tool doesn't like indentation changes).
2020-06-19Add Match utility function. (#4632)Abdalrhman Mohamed
2020-06-19(proof-new) Make static methods in re-elim (#4623)Andrew Reynolds
In preparation for coarse-grained rule for re-elim to be used by the solver and proof checker.
2020-06-19(proof-new) CDProof inherits from ProofGenerator (#4622)Andrew Reynolds
This design simplifies a number of issues and makes the PRefProofGenerator class obsolete.
2020-06-19Add casc j10 scripts (#4621)Andrew Reynolds
Adds scripts submitted to CASC competition. Note that this version of CVC4 submitted to CASC was modified to allow models when --sort-inference is enabled, since model output is required.
2020-06-19(proof-new) Updates to strings term registry (#4599)Andrew Reynolds
This makes it so that methods for constructing term registration lemmas are made into static methods, so that they can be used by both the term registry and proof checker.
2020-06-19Convert more uses of strings to words (#4584)Andrew Reynolds
Towards theory of sequences. This PR also adds support for sequences in default sygus grammars. Also removes an interface for mkEmptyWord which doesn't have an equivalent for sequences.
2020-06-19(proof-new) Split operator elimination from arithmetic (#4581)Andrew Reynolds
This class will be undergoing further refactoring for the sake of proofs. This also makes several classes of skolems context-independent instead of user-context-dependent, since this is the expected policy for skolems. Note these skolems will eventually be incorporated into the SkolemManager utility.
2020-06-19Clean the header file of TheoryStrings (#4272)Andrew Reynolds
Now conforms to coding guidelines. For the sake of ensuring that the aspects related to the strategy were maintained in one place, I split this to its own file, strategy.h/cpp.
2020-06-19Update version information post 1.8 release (#4635)Andres Noetzli
2020-06-19Always rewrite boolean ITEs with constant then/else-branches (#4619)Haniel Barbosa
Also adds better tracing and rewrites for binary AND/OR to account for reductions from constant ITEs. An evaluation of master vs this commit, with 600s, no options, shows the impact of this commit to be negligible and mostly restricted to QF_LIA. Below there is a summary and a list of the unique solves. ``` Benchmark | Stat Slvd Tot To Mo Err Cpu[s] Mem[MB] Uniq | Stat Slvd Tot To Mo Err Cpu[s] Mem[MB] Uniq | QF_ALIA | ok 125 126 1 0 0 2382.6 5410.8 0 | ok 125 126 1 0 0 2322.1 5211.8 0 | QF_AX | ok 549 551 2 0 0 2381.4 2533.1 0 | ok 549 551 2 0 0 2400.8 2676.4 0 | QF_IDL | ok 1682 2193 511 0 0 399395.4 491490.3 3 | ok 1682 2193 511 0 0 400813.9 491129.9 3 | QF_LIA | ok 4419 6947 2521 7 0 1774140.9 2782838.1 27 | ok 4409 6947 2531 7 0 1775886.7 2785165.7 17 | QF_LIRA | ok 5 7 2 0 0 1209.9 3626.9 0 | ok 5 7 2 0 0 1209.5 3707.2 0 | QF_LRA | ok 1517 1648 131 0 0 134215.1 170443.1 3 | ok 1516 1648 132 0 0 134819.6 169942.7 2 | QF_RDL | ok 210 255 45 0 0 32896.0 23261.0 0 | ok 210 255 45 0 0 32902.7 23312.5 0 | QF_UF | ok 7444 7457 13 0 0 16156.4 74432.9 0 | ok 7444 7457 13 0 0 16043.8 75067.6 0 | __totals | ok 15951 19184 3226 7 0 2362777.7 3554036.2 33 | ok 15940 19184 3237 7 0 2366399.2 3556213.8 22 |``` ``` DIRECTORY | master | branch | Benchmark | Stat RES Exit Cpu[s] Mem[MB] | Stat RES Exit Cpu[s] Mem[MB] | non_incremental_QF_IDL/asp-GraphPartitioning-rand_21_150_1235870252_0_k=3_v=10_e=20_unsat.gph.smt2 | to - 2 600.1 246.4 | ok 20 0 596.71 245.9 | non_incremental_QF_IDL/asp-SchurNumbers-15.13.schur.lp.smt2 | ok 10 0 533.64 243.8 | to - 2 600.07 246.8 | non_incremental_QF_IDL/job_shop-jobshop38-2-19-19-4-4-12.smt2 | ok 10 0 586.13 221.5 | to - 2 600.09 216.8 | non_incremental_QF_IDL/queens_bench-n_queen-queen82-1.smt2 | to - 2 600.01 197.8 | ok 10 0 570.36 198.9 | non_incremental_QF_IDL/schedulingIDL-tai_15x15_3_mkspan871.smt2 | to - 2 600.1 128.0 | ok 10 0 586.8 127.8 | non_incremental_QF_IDL/schedulingIDL-tai_15x15_9_mkspan930.smt2 | ok 10 0 575.55 124.4 | to - 2 600.07 122.6 | non_incremental_QF_LIA/arctic-matrix-constraint-1007795.smt2 | ok 10 0 334.96 386.7 | to - 2 600.02 335.5 | non_incremental_QF_LIA/arctic-matrix-constraint-1008025.smt2 | ok 10 0 180.57 384.6 | to - 2 600.02 338.6 | non_incremental_QF_LIA/arctic-matrix-constraint-1107622.smt2 | ok 10 0 310.68 349.2 | to - 2 600.01 341.3 | non_incremental_QF_LIA/arctic-matrix-constraint-1275621.smt2 | ok 10 0 5.59 232.0 | to - 2 600.04 407.4 | non_incremental_QF_LIA/arctic-matrix-constraint-1360077.smt2 | ok 10 0 422.4 667.7 | to - 11 591.94 663.2 | non_incremental_QF_LIA/arctic-matrix-constraint-1765766.smt2 | to - 11 598.02 656.8 | ok 10 0 62.5 669.8 | non_incremental_QF_LIA/arctic-matrix-constraint-391798.smt2 | ok 10 0 9.0 119.3 | to - 2 600.08 131.8 | non_incremental_QF_LIA/arctic-matrix-constraint-481231.smt2 | ok 10 0 402.37 220.9 | to - 2 600.09 199.6 | non_incremental_QF_LIA/arctic-matrix-constraint-689472.smt2 | ok 10 0 28.51 155.9 | to - 2 600.06 215.1 | non_incremental_QF_LIA/arctic-matrix-constraint-864173.smt2 | ok 10 0 125.59 326.3 | to - 11 597.87 348.8 | non_incremental_QF_LIA/arctic-matrix-constraint-901628.smt2 | to - 2 600.04 225.5 | ok 10 0 391.31 228.3 | non_incremental_QF_LIA/arctic-matrix-constraint-916576.smt2 | to - 2 600.01 244.4 | ok 10 0 432.4 246.9 | non_incremental_QF_LIA/arctic-matrix-constraint-928134.smt2 | ok 10 0 447.55 222.7 | to - 2 600.06 264.7 | non_incremental_QF_LIA/nec-smt-large-checkpass_pwd-prp-27-42.smt2 | ok 10 0 579.39 414.9 | to - 2 600.07 417.4 | non_incremental_QF_LIA/nec-smt-large-checkpass_pwd-prp-27-47.smt2 | to - 2 600.02 604.2 | ok 10 0 594.54 603.6 | non_incremental_QF_LIA/nec-smt-large-checkpass_pwd-prp-45-43.smt2 | to - 2 600.05 628.1 | ok 10 0 588.25 627.6 | non_incremental_QF_LIA/nec-smt-large-checkpass_pwd-prp-46-47.smt2 | ok 10 0 589.88 570.0 | to - 2 600.09 566.9 | non_incremental_QF_LIA/nec-smt-large-checkpass_pwd-prp-54-47.smt2 | ok 20 0 590.89 599.9 | to - 2 600.01 598.4 | non_incremental_QF_LIA/nec-smt-large-checkpass_pwd-prp-54-50.smt2 | ok 10 0 594.72 804.7 | to - 11 593.13 843.5 | non_incremental_QF_LIA/nec-smt-large-getoption_group-prp-17-47.smt2 | ok 20 0 593.29 524.2 | to - 2 600.08 522.8 | non_incremental_QF_LIA/nec-smt-large-getoption_group-prp-20-48.smt2 | to - 2 600.02 562.5 | ok 10 0 594.33 560.3 | non_incremental_QF_LIA/nec-smt-large-getoption_group-prp-5-46.smt2 | to - 2 600.09 492.9 | ok 10 0 576.02 491.9 | non_incremental_QF_LIA/nec-smt-large-getoption_group-prp-52-47.smt2 | to - 2 600.02 532.2 | ok 20 0 592.3 533.4 | non_incremental_QF_LIA/nec-smt-large-getoption_group-prp-53-48.smt2 | ok 20 0 599.82 729.4 | to - 2 600.02 742.1 | non_incremental_QF_LIA/nec-smt-large-getoption_user-prp-41-47.smt2 | to - 11 589.46 1377.2 | ok 20 0 580.82 1380.1 | non_incremental_QF_LIA/nec-smt-large-user_is_in_group-prp-23-46.smt2 | to - 2 600.08 633.5 | ok 10 0 576.07 634.0 | non_incremental_QF_LIA/tropical-matrix-constraint-1015084.smt2 | ok 10 0 408.08 374.5 | to - 2 600.01 336.4 | non_incremental_QF_LIA/tropical-matrix-constraint-1206577.smt2 | ok 10 0 361.82 375.4 | to - 11 593.45 288.4 | non_incremental_QF_LIA/tropical-matrix-constraint-1268455.smt2 | ok 10 0 270.87 654.3 | to - 2 600.08 670.5 | non_incremental_QF_LIA/tropical-matrix-constraint-1270163.smt2 | to - 2 600.02 410.4 | ok 10 0 425.02 420.6 | non_incremental_QF_LIA/tropical-matrix-constraint-1270998.smt2 | ok 10 0 349.91 384.6 | to - 2 600.01 417.5 | non_incremental_QF_LIA/tropical-matrix-constraint-1290859.smt2 | to - 2 600.1 365.9 | ok 10 0 117.77 270.0 | non_incremental_QF_LIA/tropical-matrix-constraint-1361831.smt2 | to - 2 600.07 431.0 | ok 10 0 421.55 686.9 | non_incremental_QF_LIA/tropical-matrix-constraint-1452366.smt2 | to - 2 600.04 439.4 | ok 10 0 87.42 451.9 | non_incremental_QF_LIA/tropical-matrix-constraint-1791895.smt2 | to - 2 600.1 480.3 | ok 10 0 102.16 459.7 | non_incremental_QF_LIA/tropical-matrix-constraint-1908553.smt2 | to - 2 600.01 713.8 | ok 10 0 22.22 394.9 | non_incremental_QF_LIA/tropical-matrix-constraint-2061672.smt2 | ok 10 0 51.6 521.2 | to - 2 600.04 545.8 | non_incremental_QF_LIA/tropical-matrix-constraint-244431.smt2 | ok 10 0 292.95 88.2 | to - 2 600.01 97.7 | non_incremental_QF_LIA/tropical-matrix-constraint-368069.smt2 | to - 2 600.05 135.3 | ok 10 0 445.93 134.2 | non_incremental_QF_LIA/tropical-matrix-constraint-369883.smt2 | ok 10 0 510.59 134.2 | to - 2 600.01 127.7 | non_incremental_QF_LIA/tropical-matrix-constraint-527358.smt2 | ok 10 0 243.33 135.0 | to - 2 600.05 140.7 | non_incremental_QF_LIA/tropical-matrix-constraint-614657.smt2 | ok 10 0 515.89 209.6 | to - 2 600.07 166.6 | non_incremental_QF_LIA/tropical-matrix-constraint-645054.smt2 | ok 10 0 41.34 185.3 | to - 2 600.08 205.1 | non_incremental_QF_LIA/tropical-matrix-constraint-794687.smt2 | ok 10 0 502.03 235.3 | to - 2 600.07 242.0 | non_incremental_QF_LRA/LassoRanker-CooperatingT2-sas2.t2.c_Iteration7_Loop_7-phaseTemplate.smt2 | ok 20 0 593.7 591.3 | to - 2 600.03 614.7 | non_incremental_QF_LRA/LassoRanker-SV-COMP-aviad_true-termination.c_Iteration1_Loop_4-phaseTemplate.smt2 | ok 10 0 594.16 738.5 | to - 2 600.03 701.6 | non_incremental_QF_LRA/LassoRanker-Ultimate-Collatz.bpl_Iteration1_Loop_2-pieceTemplate.smt2 | to - 2 600.09 711.5 | ok 20 0 593.46 711.2 | non_incremental_QF_LRA/tropical-matrix-constraint-199552.smt2 | ok 10 0 268.04 71.2 | to - 2 600.05 81.6 | non_incremental_QF_LRA/tropical-matrix-constraint-223827.smt2 | to - 2 600.06 91.9 | ok 10 0 505.07 95.9 |```
2020-06-19Update info for 1.8 release (#4633)Andres Noetzli
2020-06-19Cleanup examples (#4634)Andres Noetzli
This commit removes examples from unsupported programming languages and fixes a compilation issue in the sets-translate example. The issue arised due to changes to the `DefineFunctionCommand` in commit fd60da4a22f02f6f5b82cef3585240c1b33595e9 and wasn't detected by our CI because the sets-translate example requires Boost.
2020-06-19Generalize atom collection in old proof code (#4626)Haniel Barbosa
Before terms in assertions that are not sent to the SAT solver could be collected by the old proof code as atoms and thus expected to have a corresponding SAT variable. This commit fixes this by making the atom collection from assertions more conservative.
2020-06-18Bv to int elimination bugfix (#4435)yoni206
fix 1: ------ The wrong flag was checked in the traversal, causing an assertion error [here](https://github.com/CVC4/CVC4/blob/8236d7f9bff3aef4f7b37a15d509b8a11551401f/src/preprocessing/passes/bv_to_int.cpp#L247) This is fixed in this PR. A test was added as well. fix 2: ------ It is desirable that bv-to-bool runs before bv-to-int, but this was not the case, and is fixed in this PR. Do not merge until after competition release (label added).
2020-06-18Add logic check for define-fun(s)-rec (#4577)Andres Noetzli
This commit adds a logic check for `define-fun-rec`/`define-funs-rec` at the level of the new API that checks whether the logic is quantified and includes UF. To make sure that the parser actually executes that check, this commit converts the `DefineFunctionRecCommand` command to use the new API instead of the old one. This temporarily breaks the `exportTo` functionality for `DefineFunctionRecCommand` but this is not currently used within the CVC4 code base (and it seems unlikely that users use commands).
2020-06-18Revert "[Python] Properly destroy CVC4 object (#3753)" (#4422)Andrew V. Jones
This reverts commit bfa008a7ce13eff2f59b022e8c2d5d71d77f9ecb.
2020-06-18Improve memory management in Java bindings (#4629)Andres Noetzli
Fixes #2846. One of the challenges of the Java bindings is that the garbage collector can delete unused objects at any time in any order. This is an issue with CVC4's API because we require all `Expr`s to be deleted before the corresponding `ExprManager`. In the past, we were using `NewGlobalRef`/`DeleteGlobalRef` on the wrapper object of `ExprManager`. The problem is that we can have multiple instances of the wrapper that internally all refer to the same `ExprManager`. This commit implements a different approach where the Java wrappers hold an explicit reference to the `ExprManager`. The commit also removes some unused or unimportant API bits from the bindings.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback