summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-02-11Different heuristicdifferentIndexHeuristicAndres Noetzli
2020-02-11Change index heuristicAndres Noetzli
2020-02-11Fix reverse variant of F-Split inferenceAndres Noetzli
2020-02-11Remove `--strings-binary-csp` option (#3743)Andres Noetzli
2020-02-10Refactor `CoreSolver::processSimpleNEq()` (#3736)Andres Noetzli
2020-02-10Use example evaluation cache instead of sygus PBE (#3733)Andrew Reynolds
2020-02-10Implement LFSCArithProof::equalityType. (#3740)Alex Ozdemir
2020-02-10Add function for tightening literals (#3732)Alex Ozdemir
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
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
2020-02-07Interface for example evaluation cache utilities (#3726)Andrew Reynolds
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
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
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
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
2020-02-03Increase regression test time limit to 1200s. (#3704)Aina Niemetz
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
2020-02-03Fix cardinality of uninterpreted types when univset is not used (#3663)mudathirmahgoub
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
2020-01-31Handle `expectedType` in TheoryProofEngine (#3691)Alex Ozdemir
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
2020-01-30Make eq chain an aggressive rewrite in extended rewriter (#3679)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback