summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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.
2020-06-17Do not traverse WITNESS for partial substitutions in extended rewriter (#4630)Andrew Reynolds
Fixes #4620. The extended rewrite (and A B) ---> (and A (B * { A -> true } ) triggers an unsoundness when B contains witness terms. More generally, contextual substitution into witness terms is unsound since the skolemization of witness terms is added globally whereas the substitution corresponds to a fact that holds locally. This means that A -> true above may be added as a global constraint indirectly through witness skolemization. A general example of this unsoundness: (or (and (>= x 0) (P (witness ((z Int)) (=> (>= x 0) (= (* z z) x))))) F) rewrites to (or (and (>= x 0) (P (witness ((z Int)) (= (* z z) x)))) F) preprocesses to (and (or (and (>= x 0) (P k)) F) (= (* k k) x)) which now implies that (>= x 0) by the last conjunct, whereas this was not implied in the original formula This PR limits the kinds that can be traversed when applying substitutions in the extended rewriter, including from the rewrite above. In particular, the fix ensures that the partialSubstitute method is used in the extended rewriter when applicable, which now explicitly disallows recursion on WITNESS. Notice that this fixes contextual substitutions in the extended rewriter, but does not fix the more general issue. In particular, we still should be careful to check if contextual substitutions are applied by any other preprocessing passes.
2020-06-17Improve polynomial anyterm grammar (#3566)Haniel Barbosa
This changes the grammar construction in the case of anyterm + polynomial grammar so that the binary predicates EQUAL and LEQ are changed to unary predicates lambda x : ANYTERM. P(x, ZERO) rather than lambda xy. P(ANYTERM, ANYTERM), in which ZERO is a 0 constant of the respective type. Currently integer and bit-vectors are supported for this transformation. This avoid enumerating spurious terms and can lead to significant improvements in enumeration (although not necessarily in solving speed given the current unstable nature of ANYTERM usage).
2020-06-16Updates to NEWS. (#4628)Andrew Reynolds
2020-06-16Simplify sygus conversion script. (#4627)Abdalrhman Mohamed
2020-06-16Update copyright headers.Aina Niemetz
2020-06-16Add missing REQUIRES to new regressions. (#4625)Aina Niemetz
2020-06-16BV: Fix querying equality status in lazy bit-blaster. (#4618)Aina Niemetz
Fixes #4076. In the lazy bit-blaster, when querying the equality status, if the SAT solver has a full model, it is queried for the model values of the operands of the equality. However, the check if the bit-blaster has a full model did not consider the case where no assertions have yet been added, which leads to querying values of bits that are still unassigned in the SAT solver. Co-authored-by: <mathias.preiner@gmail.com>
2020-06-15Fix regressions in regress1 after #4613. (#4616)Aina Niemetz
2020-06-15(proof-new) Add quantifiers proof checker (#4593)Andrew Reynolds
Adds core rules for quantifiers, some of which also will be used as a general way for introducing and skolemizing witness terms. This PR also changes the order of other rules in proof_rule.h/cpp which was in an abnormal order from previous merges.
2020-06-15(proof-new) Update proof node, add proof node algorithm utility file. (#4600)Andrew Reynolds
Moves get free assumptions to a proof_node_algorithm.h/cpp file, analogous to node_algorithm.h/cpp. Adds a more general form of it, getFreeAssumptionsMap, which is required for future method ProofNodeManager::mkScope.
2020-06-15Support AND/OR definitions in lambda to array rewriting (#4615)Haniel Barbosa
This makes the conversion between lambdas and arrays, done in the theory builtin rewriter and used in higher-order model construction, robust to function definitions in terms of AND/OR. This also improves tracing and makes a few parts of the code adhere to code guidelines.
2020-06-15BV: Add missing type check for BITVECTOR_REPEAT_OP. (#4614)Aina Niemetz
Fixes #4075.
2020-06-15BV: Add missing type check for INT_TO_BITVECTOR. (#4613)Aina Niemetz
Fixes #4130. This further makes an attempt at more consistent error printing.
2020-06-15 Do RE derivation inference only for concrete constant RE (#4609)Andrew Reynolds
The RE derive inference was not designed to handle re.comp. This makes the application of this inference more conservative.
2020-06-12Move sygus datatype utility functions to their own file (#4595)Andrew Reynolds
Separates them from the core datatype utilities. Code move only.
2020-06-12Update to consistent policy for removed terms in quantifier bodies. (#4602)Andrew Reynolds
2020-06-12(proof-new) Term conversion proof generator utility (#4603)Andrew Reynolds
This utility is used for constructing any proof where a term is "converted" into another by small step rewrites. This utility will be used to construct the skeleton of the proofs of rewrites, preprocessing steps, expand definitions, results of substitutions, and so on.
2020-06-12(proof-new) Minor updates to strings base solver (#4606)Andrew Reynolds
In preparation for proofs, this PR involves flattening AND and removing spurious true literals in conjunctions. This also updates our policy for applying cardinality, where in some rare cases we were applying cardinality for pairs of string terms for length 0 (e.g. "there is at most 1 eqc of length 0"), which is spurious due to our term registry which always splits on emptiness.
2020-06-12Cardinality-related inferences per type in theory of strings (#4585)Andrew Reynolds
Towards theory of sequences. This updates various inference steps in the theory of strings that are based on collecting all equivalence classes to be per string-like type.
2020-06-11(proof-new) Split TheoryEngine (#4558)Andrew Reynolds
This PR splits two classes from TheoryEngine (EngineOutputChannel and TheoryPreprocess) that will be undergoing further refactoring for proofs. This PR does not change their behavior and is code-move only modulo a few cosmetic changes.
2020-06-11Fix install of static builds (#4604)Andres Noetzli
We use CMAKE_INSTALL_PATH to set the installation prefix as an RPATH in the executable. However, for static builds, changing the RPATH fails. This commit changes our build system to only change the CMAKE_INSTALL_PATH if we are doing a shared library build.
2020-06-11Add rewrite for str.replace_re. (#4601)Andrew Reynolds
This was discovered due to a proof checking abnormality, where the checker surprisingly succeeded in proving that the reduced form for a str.replace_re was equivalent for 2 different sets of skolems after rewriting.
2020-06-11 (proof-new) Add lazy proof utility (#4589)Andrew Reynolds
Adds an extension of CDProof where facts can be mapped to (lazy) proof generators.
2020-06-10(proof-new) Add eager proof generator utility. (#4592)Andrew Reynolds
Adds the eager proof generator. This lives in theory/ since it has utilities for generating TrustNode, which is specific to theory/.
2020-06-10(proof-new) Remove arith-snorm option. (#4591)Andrew Reynolds
This option only marginally helped and will be difficult to support with the new proof infrastructure.
2020-06-10(proof-new) Theory proof step buffer utility (#4580)Andrew Reynolds
This is a common class for adding steps for theory-specific proof rules into a ProofStepBuffer.
2020-06-10Add support for str.replace_re/str.replace_re_all (#4594)Andres Noetzli
This commit adds support for the last remaining string operators from the new SMT-LIB standard for the theory of strings. The commit adds the kinds, type checking, reductions, and evaluation rewrites for `str.replace_re` and `str.replace_re_all`.
2020-06-10Fix getKind for Python bindings (#4496)makaimann
I noticed recently that getKind for Op and Term was not correct in the python bindings. This PR would add maps to keep track of the Kind objects and the Python names (which are different from the C++ Kind names). Then a Python `kind` only needs the integer representation of a `Kind` to be constructed. Now, in `getKind` it can just pass the integer representation when constructing a `kind`.
2020-06-09(proof-new) Refactor skolemization (#4586)Andrew Reynolds
This PR refactors skolemization in SkolemManager so that we use a "curried" form, where witnesses for a variable x is based on the existential where the prefix up to x has already been skolemized. This additionally adds more utility functions that will be used in the internal proof checker for quantifiers.
2020-06-09(proof-new) Add trust node utility (#4588)Andrew Reynolds
This is a core data structure for associating a formula with a proof generator.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback