summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
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-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-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-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-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-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-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-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-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-16Update copyright headers.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-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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback