projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2020-02-19 makaimannAdd Python bindings using Cython -- see below for more... commit | commitdiff | tree
2020-02-19 Andrew ReynoldsDelay enumerative instantiation if theory engine does... commit | commitdiff | tree
2020-02-19 Andrew ReynoldsChange Record to shared_ptr (#3778) commit | commitdiff | tree
2020-02-19 Andrew ReynoldsFix approximate bounds for transcendental functions... commit | commitdiff | tree
2020-02-19 makaimannChange datatype selector/constructor/tester to terms... commit | commitdiff | tree
2020-02-18 Andrew ReynoldsAdd missing kinds for the new API (#3757) commit | commitdiff | tree
2020-02-17 Andrew ReynoldsOption to limit the number of rounds of enumerative... commit | commitdiff | tree
2020-02-17 Andrew Reynolds Fix soundness bug in reduction of integer div/mod... commit | commitdiff | tree
2020-02-17 Haniel BarbosaUsing ParseOp in TPTP (#3764) commit | commitdiff | tree
2020-02-17 Abdalrhman... Support dumping Sygus commands. (#3763) commit | commitdiff | tree
2020-02-16 Andrew ReynoldsFix simple issue with cache (#3762) commit | commitdiff | tree
2020-02-16 Andrew ReynoldsAdd temporary global API conversion utilities. (#3759) commit | commitdiff | tree
2020-02-16 Andres NoetzliActivate reverse variant of F-Split inference (#3745) commit | commitdiff | tree
2020-02-16 Andrew ReynoldsDisable regression (#3761) commit | commitdiff | tree
2020-02-15 Andrew ReynoldsMove proxy variables to InferenceManager in strings... commit | commitdiff | tree
2020-02-14 Andrew ReynoldsRemove quantifiers rewrite rules infrastructure (#3754) commit | commitdiff | tree
2020-02-14 Andrew ReynoldsUpdate sygus v1 parser to use ParseOp utility (#3756) commit | commitdiff | tree
2020-02-14 Haniel BarbosaForcing rewrite pass rather than asserting if formula... commit | commitdiff | tree
2020-02-13 Andrew ReynoldsConst input for sygus print callback (#3755) commit | commitdiff | tree
2020-02-13 Andres Noetzli[Python] Properly destroy CVC4 object (#3753) commit | commitdiff | tree
2020-02-12 Andres NoetzliRename Java package to edu.stanford.CVC4 (#3752) commit | commitdiff | tree
2020-02-12 Andrew ReynoldsEnsure ext rewrites for associative ops dont throw... commit | commitdiff | tree
2020-02-12 Mathias Preinerrun_regression: Distinguish between timeout and failure... commit | commitdiff | tree
2020-02-12 Andrew ReynoldsFix non-linear equality solving that involves mixed... commit | commitdiff | tree
2020-02-11 Mathias Preinercmake: Remove unused ENABLE_OPTIMIZED option. (#3749) commit | commitdiff | tree
2020-02-11 Andrew ReynoldsFix term simplification based on entailment in quantifi... commit | commitdiff | tree
2020-02-11 Mathias PreinerUpdate issue templates commit | commitdiff | tree
2020-02-11 Andres NoetzliRemove `--strings-binary-csp` option (#3743) commit | commitdiff | tree
2020-02-11 Andres NoetzliRefactor `CoreSolver::processSimpleNEq()` (#3736) commit | commitdiff | tree
2020-02-11 Andrew ReynoldsUse example evaluation cache instead of sygus PBE ... commit | commitdiff | tree
2020-02-11 Alex OzdemirImplement LFSCArithProof::equalityType. (#3740) commit | commitdiff | tree
2020-02-10 Alex OzdemirAdd function for tightening literals (#3732) commit | commitdiff | tree
2020-02-10 Mathias Preinercmake: Use ld.gold if available for faster link times... commit | commitdiff | tree
2020-02-10 Alex OzdemirAdd more IntReal predicates (#3731) commit | commitdiff | tree
2020-02-08 Andrew ReynoldsFix rewrite rules sat regressions (#3734) commit | commitdiff | tree
2020-02-08 Andres NoetzliMake "unknown" non-critical for unsat cores check ... commit | commitdiff | tree
2020-02-08 Andrew ReynoldsSplit strings finite model finding strategy (#3727) commit | commitdiff | tree
2020-02-08 Andrew ReynoldsSplit core solver from the theory of strings (#3713) commit | commitdiff | tree
2020-02-08 Andrew ReynoldsInterface for example evaluation cache utilities (... commit | commitdiff | tree
2020-02-07 mudathirmahgoubUniveset Cardinality constraints for infinite types... commit | commitdiff | tree
2020-02-07 Andrew ReynoldsRefactor check-model handling in SmtEngine (#3723) commit | commitdiff | tree
2020-02-07 Alex OzdemirPropagate expected types through UF arguments (#3717) commit | commitdiff | tree
2020-02-07 Alex OzdemirAdd `ArithProof::{printInteger,getLfscFunction}` (... commit | commitdiff | tree
2020-02-07 Andrew ReynoldsStatistics for fast enumerator (#3699) commit | commitdiff | tree
2020-02-07 Andrew ReynoldsExample evaluation cache utility (#3698) commit | commitdiff | tree
2020-02-07 Andrew ReynoldsFix exact sqrt (#3721) commit | commitdiff | tree
2020-02-06 Andrew ReynoldsGeneralize containsQuantifiers to hasClosure (#3722) commit | commitdiff | tree
2020-02-05 Andrew ReynoldsFix QF_NIA smt comp script (#3715) commit | commitdiff | tree
2020-02-04 mudathirmahgoubUpdate INSTALL.md (#3714) commit | commitdiff | tree
2020-02-04 Alex OzdemirArticulate proof-related debug statements in arith... commit | commitdiff | tree
2020-02-04 Aina Niemetz--fp-exp: Better warning message. (#3709) commit | commitdiff | tree
2020-02-04 Mathias PreinerFix header installation on MacOS. (#3660) commit | commitdiff | tree
2020-02-04 Andrew ReynoldsSplit base solver from the theory of strings (#3680) commit | commitdiff | tree
2020-02-04 Andres NoetzliRevert semantic change from refactoring (#3711) commit | commitdiff | tree
2020-02-04 Alex OzdemirRegression tests for arithmetic proofs. (#3701) commit | commitdiff | tree
2020-02-04 Aina NiemetzIncrease regression test time limit to 1200s. (#3704) commit | commitdiff | tree
2020-02-03 Clark BarrettFix corner case - might need to REWRITE_AGAIN (#3706) commit | commitdiff | tree
2020-02-03 Andrew ReynoldsUtility function for getting component types (#3703) commit | commitdiff | tree
2020-02-03 Andrew ReynoldsMinor fixes to regressions (#3702) commit | commitdiff | tree
2020-02-03 mudathirmahgoubFix cardinality of uninterpreted types when univset... commit | commitdiff | tree
2020-02-03 Andrew ReynoldsSplit on model values when repaired model from non... commit | commitdiff | tree
2020-02-03 Andrew ReynoldsFix invariant template inference for trivially infeasib... commit | commitdiff | tree
2020-02-03 Andrew ReynoldsFix corner case of empty domains in bounded fmf (#3690) commit | commitdiff | tree
2020-02-03 Andrew ReynoldsExample inference utility (#3670) commit | commitdiff | tree
2020-02-03 Andrew V. JonesRenaming '--bsd' to '--no-gpl' (#3609) commit | commitdiff | tree
2020-02-01 Alex OzdemirHandle `expectedType` in TheoryProofEngine (#3691) commit | commitdiff | tree
2020-01-31 Andrew ReynoldsAllow PBE symmetry breaking with sygus stream (#3686) commit | commitdiff | tree
2020-01-31 Andrew ReynoldsRefactor relevance vectors for asserted quantifiers... commit | commitdiff | tree
2020-01-31 Andrew ReynoldsUpdate sygus grammar normalization to use node-level... commit | commitdiff | tree
2020-01-31 Andrew ReynoldsRefactor sygus stats (#3684) commit | commitdiff | tree
2020-01-31 Andrew ReynoldsMinor refactoring of constructor classes in fast enumer... commit | commitdiff | tree
2020-01-31 Andres NoetzliFix arithmetic rewriter for exponential (#3688) commit | commitdiff | tree
2020-01-30 Andrew ReynoldsFix rep set increment for empty domains (#3682) commit | commitdiff | tree
2020-01-30 Andrew ReynoldsMake eq chain an aggressive rewrite in extended rewrite... commit | commitdiff | tree
2020-01-30 Andrew ReynoldsEliminate spurious postprocessing step for single invoc... commit | commitdiff | tree
2020-01-30 Andrew ReynoldsEnsure literals in FMF decision strategies are in the... commit | commitdiff | tree
2020-01-30 Andrew ReynoldsWeaken assertion for models with approximations (#3667) commit | commitdiff | tree
2020-01-30 Andrew ReynoldsMove disequality list to solver state in strings (... commit | commitdiff | tree
2020-01-30 Andrew ReynoldsExample minimize evaluation utility. (#3671) commit | commitdiff | tree
2020-01-30 Andrew ReynoldsExternal cache argument for evaluator (#3672) commit | commitdiff | tree
2020-01-30 Andrew ReynoldsDo not debug check model for models with approximations... commit | commitdiff | tree
2020-01-30 Andres NoetzliBetter heuristics for marking congruent variables ... commit | commitdiff | tree
2020-01-30 Andrew ReynoldsModularize more steps in the strings strategy (#3676) commit | commitdiff | tree
2020-01-30 Andrew ReynoldsMinor updates to string utilities (#3675) commit | commitdiff | tree
2020-01-30 Alex OzdemirexpectedType in proof-printing code (#3665) commit | commitdiff | tree
2020-01-29 Andrew ReynoldsFix isLeq function in String utility (#3659) commit | commitdiff | tree
2020-01-28 Andrew ReynoldsDo not insist on bound values being constant in arithme... commit | commitdiff | tree
2020-01-28 Andrew ReynoldsAvoid PLUS with one child for bv2nat elimination (... commit | commitdiff | tree
2020-01-26 Alex OzdemirAxioms for affine function bounds. Tests. (#3632) commit | commitdiff | tree
2020-01-23 Andrew ReynoldsFix trivial solve method for single invocation (#3650) commit | commitdiff | tree
2020-01-22 Andrew ReynoldsFix subtyping for instantiations where internal represe... commit | commitdiff | tree
2020-01-22 Andrew ReynoldsFix substitution in nl solver (#3638) commit | commitdiff | tree
2020-01-22 Andrew ReynoldsFix single invocation partition for non-function non... commit | commitdiff | tree
2020-01-22 Andrew ReynoldsFix check for subtypes in sygus PBE (#3640) commit | commitdiff | tree
2020-01-22 Andrew ReynoldsFix parameteric sorts involving Booleans in sygus defau... commit | commitdiff | tree
2020-01-21 Alex OzdemirTypes and side conditions for affine bounds (#3631) commit | commitdiff | tree
2020-01-21 Alex OzdemirAffine Axioms (#3630) commit | commitdiff | tree
2020-01-21 Alex OzdemirTypes & side-conditions for linear and affine fns ... commit | commitdiff | tree
2020-01-21 Alex OzdemirAxioms (and side conditions) for tightening bounds... commit | commitdiff | tree
2020-01-18 Alex OzdemirLIRA proof: Arithmetic predicates & reification thereof... commit | commitdiff | tree
next