projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Add missing kinds for the new API (#3757)
2020-02-18
Andrew Reynolds
Add missing kinds for the new API (#3757)
commit
|
commitdiff
|
tree
2020-02-17
Andrew Reynolds
Option 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...
...introduced 7 years ago in https://
github
.com/CVC4/CVC4/commit/9098391fe334d829ec...
commit
|
commitdiff
|
tree
2020-02-17
Haniel Barbosa
Using ParseOp in TPTP (#3764)
commit
|
commitdiff
|
tree
2020-02-17
Abdalrhman Mohamed
Support dumping Sygus commands. (#3763)
commit
|
commitdiff
|
tree
2020-02-16
Andrew Reynolds
Fix simple issue with cache (#3762)
commit
|
commitdiff
|
tree
2020-02-16
Andrew Reynolds
Add temporary global API conversion utilities. (#3759)
commit
|
commitdiff
|
tree
2020-02-16
Andres Noetzli
Activate reverse variant of F-Split inference (#3745)
commit
|
commitdiff
|
tree
2020-02-16
Andrew Reynolds
Disable regression (#3761)
commit
|
commitdiff
|
tree
2020-02-15
Andrew Reynolds
Move proxy variables to InferenceManager in strings...
commit
|
commitdiff
|
tree
2020-02-14
Andrew Reynolds
Remove quantifiers rewrite rules infrastructure (#3754)
commit
|
commitdiff
|
tree
2020-02-14
Andrew Reynolds
Update sygus v1 parser to use ParseOp utility (#3756)
commit
|
commitdiff
|
tree
2020-02-14
Haniel Barbosa
Forcing rewrite pass rather than asserting if formula...
commit
|
commitdiff
|
tree
2020-02-13
Andrew Reynolds
Const 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 Noetzli
Rename Java package to edu.stanford.CVC4 (#3752)
commit
|
commitdiff
|
tree
2020-02-12
Andrew Reynolds
Ensure ext rewrites for associative ops dont throw...
commit
|
commitdiff
|
tree
2020-02-12
Mathias Preiner
run_regression: Distinguish between timeout and failure...
commit
|
commitdiff
|
tree
2020-02-12
Andrew Reynolds
Fix non-linear equality solving that involves mixed...
...43099566+ahmed-irfan@users.noreply.
github
.com>
commit
|
commitdiff
|
tree
2020-02-11
Mathias Preiner
cmake: Remove unused ENABLE_OPTIMIZED option. (#3749)
commit
|
commitdiff
|
tree
2020-02-11
Andrew Reynolds
Fix term simplification based on entailment in quantifiers...
commit
|
commitdiff
|
tree
2020-02-11
Mathias Preiner
Update issue templates
commit
|
commitdiff
|
tree
2020-02-11
Andres Noetzli
Remove `--strings-binary-csp` option (#3743)
commit
|
commitdiff
|
tree
2020-02-11
Andres Noetzli
Refactor `CoreSolver::processSimpleNEq()` (#3736)
commit
|
commitdiff
|
tree
2020-02-11
Andrew Reynolds
Use example evaluation cache instead of sygus PBE ...
commit
|
commitdiff
|
tree
2020-02-11
Alex Ozdemir
Implement LFSCArithProof::equalityType. (#3740)
commit
|
commitdiff
|
tree
2020-02-10
Alex Ozdemir
Add function for tightening literals (#3732)
commit
|
commitdiff
|
tree
2020-02-10
Mathias Preiner
cmake: Use ld.gold if available for faster link times...
commit
|
commitdiff
|
tree
2020-02-10
Alex Ozdemir
Add more IntReal predicates (#3731)
commit
|
commitdiff
|
tree
2020-02-08
Andrew Reynolds
Fix rewrite rules sat regressions (#3734)
commit
|
commitdiff
|
tree
2020-02-08
Andres Noetzli
Make "unknown" non-critical for unsat cores check ...
commit
|
commitdiff
|
tree
2020-02-08
Andrew Reynolds
Split strings finite model finding strategy (#3727)
commit
|
commitdiff
|
tree
2020-02-08
Andrew Reynolds
Split core solver from the theory of strings (#3713)
commit
|
commitdiff
|
tree
2020-02-08
Andrew Reynolds
Interface for example evaluation cache utilities (...
commit
|
commitdiff
|
tree
2020-02-07
mudathirmahgoub
Univeset Cardinality constraints for infinite types...
commit
|
commitdiff
|
tree
2020-02-07
Andrew Reynolds
Refactor check-model handling in SmtEngine (#3723)
commit
|
commitdiff
|
tree
2020-02-07
Alex Ozdemir
Propagate expected types through UF arguments (#3717)
commit
|
commitdiff
|
tree
2020-02-07
Alex Ozdemir
Add `ArithProof::{printInteger,getLfscFunction}` (...
commit
|
commitdiff
|
tree
2020-02-07
Andrew Reynolds
Statistics for fast enumerator (#3699)
commit
|
commitdiff
|
tree
2020-02-07
Andrew Reynolds
Example evaluation cache utility (#3698)
commit
|
commitdiff
|
tree
2020-02-07
Andrew Reynolds
Fix exact sqrt (#3721)
...43099566+ahmed-irfan@users.noreply.
github
.com>
commit
|
commitdiff
|
tree
2020-02-06
Andrew Reynolds
Generalize containsQuantifiers to hasClosure (#3722)
commit
|
commitdiff
|
tree
2020-02-05
Andrew Reynolds
Fix QF_NIA smt comp script (#3715)
commit
|
commitdiff
|
tree
2020-02-04
mudathirmahgoub
Update INSTALL.md (#3714)
commit
|
commitdiff
|
tree
2020-02-04
Alex Ozdemir
Articulate 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 Preiner
Fix header installation on MacOS. (#3660)
commit
|
commitdiff
|
tree
2020-02-04
Andrew Reynolds
Split base solver from the theory of strings (#3680)
commit
|
commitdiff
|
tree
2020-02-04
Andres Noetzli
Revert semantic change from refactoring (#3711)
commit
|
commitdiff
|
tree
2020-02-04
Alex Ozdemir
Regression tests for arithmetic proofs. (#3701)
commit
|
commitdiff
|
tree
2020-02-04
Aina Niemetz
Increase regression test time limit to 1200s. (#3704)
commit
|
commitdiff
|
tree
2020-02-03
Clark Barrett
Fix corner case - might need to REWRITE_AGAIN (#3706)
commit
|
commitdiff
|
tree
2020-02-03
Andrew Reynolds
Utility function for getting component types (#3703)
commit
|
commitdiff
|
tree
2020-02-03
Andrew Reynolds
Minor fixes to regressions (#3702)
commit
|
commitdiff
|
tree
2020-02-03
mudathirmahgoub
Fix cardinality of uninterpreted types when univset...
commit
|
commitdiff
|
tree
2020-02-03
Andrew Reynolds
Split on model values when repaired model from non...
commit
|
commitdiff
|
tree
2020-02-03
Andrew Reynolds
Fix invariant template inference for trivially infeasible...
commit
|
commitdiff
|
tree
2020-02-03
Andrew Reynolds
Fix corner case of empty domains in bounded fmf (#3690)
commit
|
commitdiff
|
tree
2020-02-03
Andrew Reynolds
Example inference utility (#3670)
commit
|
commitdiff
|
tree
2020-02-03
Andrew V. Jones
Renaming '--bsd' to '--no-gpl' (#3609)
commit
|
commitdiff
|
tree
2020-02-01
Alex Ozdemir
Handle `expectedType` in TheoryProofEngine (#3691)
commit
|
commitdiff
|
tree
2020-01-31
Andrew Reynolds
Allow PBE symmetry breaking with sygus stream (#3686)
commit
|
commitdiff
|
tree
2020-01-31
Andrew Reynolds
Refactor relevance vectors for asserted quantifiers...
commit
|
commitdiff
|
tree
2020-01-31
Andrew Reynolds
Update sygus grammar normalization to use node-level...
commit
|
commitdiff
|
tree
2020-01-31
Andrew Reynolds
Refactor sygus stats (#3684)
commit
|
commitdiff
|
tree
2020-01-31
Andrew Reynolds
Minor refactoring of constructor classes in fast enumerator...
commit
|
commitdiff
|
tree
2020-01-31
Andres Noetzli
Fix arithmetic rewriter for exponential (#3688)
commit
|
commitdiff
|
tree
2020-01-30
Andrew Reynolds
Fix rep set increment for empty domains (#3682)
commit
|
commitdiff
|
tree
2020-01-30
Andrew Reynolds
Make eq chain an aggressive rewrite in extended rewriter...
commit
|
commitdiff
|
tree
2020-01-30
Andrew Reynolds
Eliminate spurious postprocessing step for single invocation...
commit
|
commitdiff
|
tree
2020-01-30
Andrew Reynolds
Ensure literals in FMF decision strategies are in the...
commit
|
commitdiff
|
tree
2020-01-30
Andrew Reynolds
Weaken assertion for models with approximations (#3667)
commit
|
commitdiff
|
tree
2020-01-30
Andrew Reynolds
Move disequality list to solver state in strings (...
commit
|
commitdiff
|
tree
2020-01-30
Andrew Reynolds
Example minimize evaluation utility. (#3671)
commit
|
commitdiff
|
tree
2020-01-30
Andrew Reynolds
External cache argument for evaluator (#3672)
commit
|
commitdiff
|
tree
2020-01-30
Andrew Reynolds
Do not debug check model for models with approximations...
commit
|
commitdiff
|
tree
2020-01-30
Andres Noetzli
Better heuristics for marking congruent variables ...
commit
|
commitdiff
|
tree
2020-01-30
Andrew Reynolds
Modularize more steps in the strings strategy (#3676)
commit
|
commitdiff
|
tree
2020-01-30
Andrew Reynolds
Minor updates to string utilities (#3675)
commit
|
commitdiff
|
tree
2020-01-30
Alex Ozdemir
expectedType in proof-printing code (#3665)
commit
|
commitdiff
|
tree
2020-01-29
Andrew Reynolds
Fix isLeq function in String utility (#3659)
commit
|
commitdiff
|
tree
2020-01-28
Andrew Reynolds
Do not insist on bound values being constant in arithmetic...
commit
|
commitdiff
|
tree
2020-01-28
Andrew Reynolds
Avoid PLUS with one child for bv2nat elimination (...
commit
|
commitdiff
|
tree
2020-01-26
Alex Ozdemir
Axioms for affine function bounds. Tests. (#3632)
...yoni206 <yoni206@users.noreply.
github
.com>
...yoni206 <yoni206@users.noreply.
github
.com>
commit
|
commitdiff
|
tree
2020-01-23
Andrew Reynolds
Fix trivial solve method for single invocation (#3650)
commit
|
commitdiff
|
tree
2020-01-22
Andrew Reynolds
Fix subtyping for instantiations where internal representati...
commit
|
commitdiff
|
tree
2020-01-22
Andrew Reynolds
Fix substitution in nl solver (#3638)
...43099566+ahmed-irfan@users.noreply.
github
.com>
commit
|
commitdiff
|
tree
2020-01-22
Andrew Reynolds
Fix single invocation partition for non-function non...
commit
|
commitdiff
|
tree
2020-01-22
Andrew Reynolds
Fix check for subtypes in sygus PBE (#3640)
commit
|
commitdiff
|
tree
2020-01-22
Andrew Reynolds
Fix parameteric sorts involving Booleans in sygus default...
commit
|
commitdiff
|
tree
2020-01-21
Alex Ozdemir
Types and side conditions for affine bounds (#3631)
commit
|
commitdiff
|
tree
2020-01-21
Alex Ozdemir
Affine Axioms (#3630)
commit
|
commitdiff
|
tree
2020-01-21
Alex Ozdemir
Types & side-conditions for linear and affine fns ...
commit
|
commitdiff
|
tree
2020-01-21
Alex Ozdemir
Axioms (and side conditions) for tightening bounds...
...yoni206 <yoni206@users.noreply.
github
.com>
...yoni206 <yoni206@users.noreply.
github
.com>
commit
|
commitdiff
|
tree
2020-01-18
Alex Ozdemir
LIRA proof: Arithmetic predicates & reification thereof...
commit
|
commitdiff
|
tree
2020-01-17
Alex Ozdemir
LIRA sig: int, real terms, and conversions (#3610)
commit
|
commitdiff
|
tree
2020-01-17
Andrew Reynolds
Use axioms when checking goal entailment for abduction...
commit
|
commitdiff
|
tree
2020-01-15
Aina Niemetz
New C++ API: Add nullary constructor for Result. (...
commit
|
commitdiff
|
tree
2020-01-14
Andrew Reynolds
Generalize example-based sym breaking to conjectures...
commit
|
commitdiff
|
tree
2020-01-14
Andres Noetzli
Disable unsat cores for regression that times out ...
commit
|
commitdiff
|
tree
next