Age | Commit message (Collapse) | Author | |
---|---|---|---|
2020-02-06 | Generalize containsQuantifiers to hasClosure (#3722) | Andrew Reynolds | |
2020-02-04 | Fix QF_NIA smt comp script (#3715) | Andrew Reynolds | |
2020-02-04 | Update INSTALL.md (#3714) | mudathirmahgoub | |
Co-authored-by: Mathias Preiner <mathias.preiner@gmail.com> | |||
2020-02-04 | Articulate proof-related debug statements in arith (#3700) | Alex Ozdemir | |
2020-02-04 | --fp-exp: Better warning message. (#3709) | Aina Niemetz | |
2020-02-04 | Fix header installation on MacOS. (#3660) | Mathias Preiner | |
On MacOS sed -i requires a suffix to be set. | |||
2020-02-04 | Split base solver from the theory of strings (#3680) | Andrew Reynolds | |
2020-02-04 | Revert semantic change from refactoring (#3711) | Andres Noetzli | |
2020-02-03 | Regression tests for arithmetic proofs. (#3701) | Alex Ozdemir | |
* Add more arith proof regression tests These tests are designed to test interesting cases of arithmetic proofs, such as mixing integers and reals and tightening bounds. Right now, they have the --no-check-proofs flag set, which prevents them from testing the proof machinery. However, once we check that machinery into master, we'll remove that flag, thus enabling the full effect of the tests. * A few comments explaining things. * Add another tightening test * Add new test to CMake * No --no-check-models. There are no models anyway. * Delete smt-lib-version, per Yoni | |||
2020-02-03 | Increase regression test time limit to 1200s. (#3704) | Aina Niemetz | |
Fixes #3565. | |||
2020-02-03 | Fix corner case - might need to REWRITE_AGAIN (#3706) | Clark Barrett | |
2020-02-03 | Utility function for getting component types (#3703) | Andrew Reynolds | |
2020-02-03 | Minor fixes to regressions (#3702) | Andrew Reynolds | |
Fixes two issues in regressions, fixes regress1. | |||
2020-02-03 | Fix cardinality of uninterpreted types when univset is not used (#3663) | mudathirmahgoub | |
* Fixed bug 3662 * format * small change * added bug3663.smt2 file * throw Logic Exception * throw Logic Exception * ;EXIT: 1 Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com> | |||
2020-02-03 | Split on model values when repaired model from non-linear is inconsisent (#3668) | Andrew Reynolds | |
2020-02-03 | Fix invariant template inference for trivially infeasible conjecture (#3693) | Andrew Reynolds | |
2020-02-03 | Fix corner case of empty domains in bounded fmf (#3690) | Andrew Reynolds | |
2020-02-03 | Example inference utility (#3670) | Andrew Reynolds | |
2020-02-02 | Renaming '--bsd' to '--no-gpl' (#3609) | Andrew V. Jones | |
Signed-off-by: Andrew V. Jones <andrew.jones@vector.com> | |||
2020-01-31 | Handle `expectedType` in TheoryProofEngine (#3691) | Alex Ozdemir | |
`TheoryProofEngine` now uses the `expectedType` optional argument. * When printing terms, it sets this for theories that it dispatches too * It occasionally asks theories for help determining the `expectedType` using `equalityType`, which has a sensible default implementation. * It is mindful of `expectedType` when using the let map. I also moved to hpp function implementations into the cpp. | |||
2020-01-31 | Allow PBE symmetry breaking with sygus stream (#3686) | Andrew Reynolds | |
2020-01-31 | Refactor relevance vectors for asserted quantifiers (#3666) | Andrew Reynolds | |
2020-01-31 | Update sygus grammar normalization to use node-level datatype. (#3567) | Andrew Reynolds | |
2020-01-31 | Refactor sygus stats (#3684) | Andrew Reynolds | |
2020-01-31 | Minor refactoring of constructor classes in fast enumerator (#3685) | Andrew Reynolds | |
2020-01-31 | Fix arithmetic rewriter for exponential (#3688) | Andres Noetzli | |
2020-01-30 | Fix rep set increment for empty domains (#3682) | Andrew Reynolds | |
2020-01-30 | Make eq chain an aggressive rewrite in extended rewriter (#3679) | Andrew Reynolds | |
2020-01-30 | Eliminate spurious postprocessing step for single invocation (#3674) | Andrew Reynolds | |
2020-01-30 | Ensure literals in FMF decision strategies are in the CNF stream (#3669) | Andrew Reynolds | |
2020-01-30 | Weaken assertion for models with approximations (#3667) | Andrew Reynolds | |
2020-01-30 | Move disequality list to solver state in strings (#3678) | Andrew Reynolds | |
2020-01-30 | Example minimize evaluation utility. (#3671) | Andrew Reynolds | |
2020-01-30 | External cache argument for evaluator (#3672) | Andrew Reynolds | |
2020-01-30 | Do not debug check model for models with approximations (#3673) | Andrew Reynolds | |
We don't run check-model for models with approximate values, however we were still running the internal debugCheckModel method, which leads to assertion failures. This disables this check. Fixes #3652. | |||
2020-01-29 | Better heuristics for marking congruent variables (#3677) | Andres Noetzli | |
2020-01-29 | Modularize more steps in the strings strategy (#3676) | Andrew Reynolds | |
2020-01-29 | Minor updates to string utilities (#3675) | Andrew Reynolds | |
2020-01-29 | expectedType in proof-printing code (#3665) | Alex Ozdemir | |
* expectedType in proof-printing code To print lemma proofs in theories that use multiple sorts that have a subtype relationship, we need to increase communication between the TheoryProofEngine and the theory proofs themselves. This commit add an (optional) argument `expectedType` to many term-printing functions in TheoryProofEngine and TheoryProof. Right now it is unused, so always takes on the default value of "null" (meaning no type expectation), but in the future the TheoryProofEngine will use it to signal TheoryProof about what type is expected to be printed. * TypeNode, Don't mix default args & virtual * Use TypeNode instead of Type (The former are lighter) * Don't add default arguments to virtual functions, because these cannot be dynamically overriden during a dynamic dispatch. * Since we don't want them to be overidable anyway, we use two functions: one that is non-virtual and has a default, the other that is virtual but has no default. The former just calls the latter. * clang-format after signature changes | |||
2020-01-29 | Fix isLeq function in String utility (#3659) | Andrew Reynolds | |
2020-01-28 | Do not insist on bound values being constant in arithmetic instantiation (#3643) | Andrew Reynolds | |
2020-01-28 | Avoid PLUS with one child for bv2nat elimination (#3639) | Andrew Reynolds | |
2020-01-25 | Axioms for affine function bounds. Tests. (#3632) | Alex Ozdemir | |
* Axioms for affine function bounds. Tests. * Apply suggestions from code review Co-Authored-By: yoni206 <yoni206@users.noreply.github.com> * Clarify descriptions of th_lira tests Thanks, Yoni! Co-authored-by: yoni206 <yoni206@users.noreply.github.com> | |||
2020-01-23 | Fix trivial solve method for single invocation (#3650) | Andrew Reynolds | |
2020-01-22 | Fix subtyping for instantiations where internal representatives are chosen ↵ | Andrew Reynolds | |
(#3641) | |||
2020-01-22 | Fix substitution in nl solver (#3638) | Andrew Reynolds | |
* Fix for 3614 * Add regression * Remove regression Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com> | |||
2020-01-22 | Fix single invocation partition for non-function non-atomic types (#3642) | Andrew Reynolds | |
2020-01-22 | Fix check for subtypes in sygus PBE (#3640) | Andrew Reynolds | |
2020-01-22 | Fix parameteric sorts involving Booleans in sygus default grammars (#3629) | Andrew Reynolds | |
2020-01-21 | Types and side conditions for affine bounds (#3631) | Alex Ozdemir | |
* Types and side conditions for affine bounds Bounds (being positive, non-negative) actually have an arithmetic. This PR defines that. Useful b/c Farkas proofs are basically just sums of bounded affine functions. * Address Yoni's comments. Thanks! * Moved a positivity-test to th_real * Describe what an affine bound is in better detail |