Age | Commit message (Collapse) | Author | |
---|---|---|---|
2020-02-11 | Refactor CoreSolver::processSimpleDeqrefactorProcessSimpleDeq | Andres Noetzli | |
2020-02-11 | Different heuristicdifferentIndexHeuristic | Andres Noetzli | |
2020-02-11 | Change index heuristic | Andres Noetzli | |
2020-02-11 | Fix reverse variant of F-Split inference | Andres Noetzli | |
This commit fixes the reverse variant of the F-Split inference. | |||
2020-02-11 | Remove `--strings-binary-csp` option (#3743) | Andres Noetzli | |
2020-02-10 | Refactor `CoreSolver::processSimpleNEq()` (#3736) | Andres Noetzli | |
This commit refactors and documents `CoreSolver::processSimpleNEq()`. This method processes equalities between normal forms. | |||
2020-02-10 | Use example evaluation cache instead of sygus PBE (#3733) | Andrew Reynolds | |
2020-02-10 | Implement LFSCArithProof::equalityType. (#3740) | Alex Ozdemir | |
Also, missed an armType use. | |||
2020-02-10 | Add function for tightening literals (#3732) | Alex Ozdemir | |
* Add function for tightening literals The function tightens a literal if it can be tightened, and prints a proof of the result. * Include a #include Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com> | |||
2020-02-10 | cmake: Use ld.gold if available for faster link times. (#3738) | Mathias Preiner | |
2020-02-10 | Add more IntReal predicates (#3731) | Alex Ozdemir | |
2020-02-08 | Fix rewrite rules sat regressions (#3734) | Andrew Reynolds | |
Quantifier rewrite rules are not robust to preprocessing within our check-model infrastructure. This disables check-model on 2 satisfiable rewrite rules regressions. Fixes nightlies. | |||
2020-02-08 | Make "unknown" non-critical for unsat cores check (#3728) | Andres Noetzli | |
2020-02-07 | Split strings finite model finding strategy (#3727) | Andrew Reynolds | |
2020-02-07 | Split core solver from the theory of strings (#3713) | Andrew Reynolds | |
This splits the main procedure from Liang et al CAV 2014 to its own file, the "core solver" of theory of strings. I have intentionally not updated or clang-formatted the code in core_solver.cpp since I would prefer this PR to involve as little change to behavior as possible (it is copied verbatim from theory_strings.cpp). Future PRs will clean this code up. | |||
2020-02-07 | Interface for example evaluation cache utilities (#3726) | Andrew Reynolds | |
This adds interfaces in synth_conjecture for getting an ExampleEvalCache, per enumerator. It also adds a specialization `checkRefinementEvalLemmas` of `getRefinementEvalLemmas` in the cegis module, which does evaluation on CEGIS refinement lemmas without structural generalization. This function will be used as an alternative to `getRefinementEvalLemmas` for fast enumerators. The next PR will update all utilities to use ExampleEvalCache instead of SygusPbe for evaluating examples. | |||
2020-02-07 | Univeset Cardinality constraints for infinite types (#3712) | mudathirmahgoub | |
2020-02-07 | Refactor check-model handling in SmtEngine (#3723) | Andrew Reynolds | |
2020-02-07 | Propagate expected types through UF arguments (#3717) | Alex Ozdemir | |
2020-02-07 | Add `ArithProof::{printInteger,getLfscFunction}` (#3716) | Alex Ozdemir | |
2020-02-07 | Statistics for fast enumerator (#3699) | Andrew Reynolds | |
2020-02-07 | Example evaluation cache utility (#3698) | Andrew Reynolds | |
2020-02-06 | Fix exact sqrt (#3721) | Andrew Reynolds | |
Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com> | |||
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 | |