Age | Commit message (Collapse) | Author | |
---|---|---|---|
2020-02-12 | Merge branch 'master' into renameJavaPackagerenameJavaPackage | Andrew Reynolds | |
2020-02-12 | Ensure ext rewrites for associative ops dont throw assertions for kind ↵ | Andrew Reynolds | |
arities (#3681) | |||
2020-02-11 | Rename Java package to edu.stanford.CVC4 | Andres Noetzli | |
Fixes #1519. | |||
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 | Fix term simplification based on entailment in quantifiers rewriter (#3746) | Andrew Reynolds | |
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-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 | 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 | 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 | 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 | |