Age | Commit message (Collapse) | Author | |
---|---|---|---|
2020-02-17 | Support dumping Sygus commands. (#3763) | Abdalrhman Mohamed | |
2020-02-16 | Fix simple issue with cache (#3762) | Andrew Reynolds | |
2020-02-16 | Add temporary global API conversion utilities. (#3759) | Andrew Reynolds | |
2020-02-16 | Activate reverse variant of F-Split inference (#3745) | Andres Noetzli | |
This commit activates the reverse variant of the F-Split inference. | |||
2020-02-15 | Disable regression (#3761) | Andrew Reynolds | |
Should fix recurring issue with nightlies. Also fixes a warning. | |||
2020-02-15 | Move proxy variables to InferenceManager in strings (#3758) | Andrew Reynolds | |
2020-02-14 | Remove quantifiers rewrite rules infrastructure (#3754) | Andrew Reynolds | |
2020-02-13 | Update sygus v1 parser to use ParseOp utility (#3756) | Andrew Reynolds | |
2020-02-13 | Forcing rewrite pass rather than asserting if formula has been rewritten (#3748) | Haniel Barbosa | |
This ensures that users or developers don't accidentally break the solver either via options or changing the SMT engine flow so that the formula is not rewritten up to a given point. | |||
2020-02-13 | Const input for sygus print callback (#3755) | Andrew Reynolds | |
2020-02-12 | [Python] Properly destroy CVC4 object (#3753) | Andres Noetzli | |
2020-02-12 | Rename Java package to edu.stanford.CVC4 (#3752) | Andres Noetzli | |
2020-02-12 | Ensure ext rewrites for associative ops dont throw assertions for kind ↵ | Andrew Reynolds | |
arities (#3681) | |||
2020-02-11 | run_regression: Distinguish between timeout and failure. (#3750) | Mathias Preiner | |
If --use-skip-return-code is enabled and a regression test times out it will return EXIT_SKIP instead of EXIT_FAILURE. | |||
2020-02-11 | Fix non-linear equality solving that involves mixed real/integer arithmetic ↵ | Andrew Reynolds | |
(#3739) * Fix non-linear equality solving that involves mixed real/integer. * Format * Fix * Revert Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com> | |||
2020-02-11 | cmake: Remove unused ENABLE_OPTIMIZED option. (#3749) | Mathias Preiner | |
2020-02-11 | Fix term simplification based on entailment in quantifiers rewriter (#3746) | Andrew Reynolds | |
2020-02-11 | Update issue templates | Mathias Preiner | |
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. |