summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-02-11Refactor CoreSolver::processSimpleDeqrefactorProcessSimpleDeqAndres Noetzli
2020-02-11Different heuristicdifferentIndexHeuristicAndres Noetzli
2020-02-11Change index heuristicAndres Noetzli
2020-02-11Fix reverse variant of F-Split inferenceAndres Noetzli
This commit fixes the reverse variant of the F-Split inference.
2020-02-11Remove `--strings-binary-csp` option (#3743)Andres Noetzli
2020-02-10Refactor `CoreSolver::processSimpleNEq()` (#3736)Andres Noetzli
This commit refactors and documents `CoreSolver::processSimpleNEq()`. This method processes equalities between normal forms.
2020-02-10Use example evaluation cache instead of sygus PBE (#3733)Andrew Reynolds
2020-02-10Implement LFSCArithProof::equalityType. (#3740)Alex Ozdemir
Also, missed an armType use.
2020-02-10Add 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-10cmake: Use ld.gold if available for faster link times. (#3738)Mathias Preiner
2020-02-10Add more IntReal predicates (#3731)Alex Ozdemir
2020-02-08Fix 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-08Make "unknown" non-critical for unsat cores check (#3728)Andres Noetzli
2020-02-07Split strings finite model finding strategy (#3727)Andrew Reynolds
2020-02-07Split 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-07Interface 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-07Univeset Cardinality constraints for infinite types (#3712)mudathirmahgoub
2020-02-07Refactor check-model handling in SmtEngine (#3723)Andrew Reynolds
2020-02-07Propagate expected types through UF arguments (#3717)Alex Ozdemir
2020-02-07Add `ArithProof::{printInteger,getLfscFunction}` (#3716)Alex Ozdemir
2020-02-07Statistics for fast enumerator (#3699)Andrew Reynolds
2020-02-07Example evaluation cache utility (#3698)Andrew Reynolds
2020-02-06Fix exact sqrt (#3721)Andrew Reynolds
Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
2020-02-06Generalize containsQuantifiers to hasClosure (#3722)Andrew Reynolds
2020-02-04Fix QF_NIA smt comp script (#3715)Andrew Reynolds
2020-02-04Update INSTALL.md (#3714)mudathirmahgoub
Co-authored-by: Mathias Preiner <mathias.preiner@gmail.com>
2020-02-04Articulate proof-related debug statements in arith (#3700)Alex Ozdemir
2020-02-04--fp-exp: Better warning message. (#3709)Aina Niemetz
2020-02-04Fix header installation on MacOS. (#3660)Mathias Preiner
On MacOS sed -i requires a suffix to be set.
2020-02-04Split base solver from the theory of strings (#3680)Andrew Reynolds
2020-02-04Revert semantic change from refactoring (#3711)Andres Noetzli
2020-02-03Regression 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-03Increase regression test time limit to 1200s. (#3704)Aina Niemetz
Fixes #3565.
2020-02-03Fix corner case - might need to REWRITE_AGAIN (#3706)Clark Barrett
2020-02-03Utility function for getting component types (#3703)Andrew Reynolds
2020-02-03Minor fixes to regressions (#3702)Andrew Reynolds
Fixes two issues in regressions, fixes regress1.
2020-02-03Fix 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-03Split on model values when repaired model from non-linear is inconsisent (#3668)Andrew Reynolds
2020-02-03Fix invariant template inference for trivially infeasible conjecture (#3693)Andrew Reynolds
2020-02-03Fix corner case of empty domains in bounded fmf (#3690)Andrew Reynolds
2020-02-03Example inference utility (#3670)Andrew Reynolds
2020-02-02Renaming '--bsd' to '--no-gpl' (#3609)Andrew V. Jones
Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>
2020-01-31Handle `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-31Allow PBE symmetry breaking with sygus stream (#3686)Andrew Reynolds
2020-01-31Refactor relevance vectors for asserted quantifiers (#3666)Andrew Reynolds
2020-01-31Update sygus grammar normalization to use node-level datatype. (#3567)Andrew Reynolds
2020-01-31Refactor sygus stats (#3684)Andrew Reynolds
2020-01-31Minor refactoring of constructor classes in fast enumerator (#3685)Andrew Reynolds
2020-01-31Fix arithmetic rewriter for exponential (#3688)Andres Noetzli
2020-01-30Fix rep set increment for empty domains (#3682)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback