projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Split expression names from SmtEngine (#4832)
[cvc5.git]
/
src
/
CMakeLists.txt
2020-08-03
Andrew Reynolds
Split expression names from SmtEngine (#4832)
blob
|
commitdiff
|
raw
2020-08-03
Andrew Reynolds
Split dump manager from SmtEngine (#4824)
blob
|
commitdiff
|
raw
|
diff to current
2020-07-31
Andrew Reynolds
Split listener classes from SmtEngine (#4816)
blob
|
commitdiff
|
raw
|
diff to current
2020-07-30
Gereon Kremer
Adds the interface for the CAD-based arithmetic solver...
blob
|
commitdiff
|
raw
|
diff to current
2020-07-28
Andrew Reynolds
Use lemma property enum for OutputChannel::lemma (...
blob
|
commitdiff
|
raw
|
diff to current
2020-07-21
Gereon Kremer
Preparations for a CAD-based arithmetic solver (#4762)
blob
|
commitdiff
|
raw
|
diff to current
2020-07-17
Andrew Reynolds
Add option manager and simpler option listener (#4745)
blob
|
commitdiff
|
raw
|
diff to current
2020-07-17
Gereon Kremer
Integration of libpoly (#4679)
blob
|
commitdiff
|
raw
|
diff to current
2020-07-16
Andrew Reynolds
Split abstract values utility from SmtEngine (#4754)
blob
|
commitdiff
|
raw
|
diff to current
2020-07-16
Haniel Barbosa
(proof-new) Adding API for converting EqProof into...
blob
|
commitdiff
|
raw
|
diff to current
2020-07-15
Andrew Reynolds
Split abduction solver from SmtEngine (#4733)
blob
|
commitdiff
|
raw
|
diff to current
2020-07-15
Gereon Kremer
Add missing header (Fixes #4743) (#4749)
blob
|
commitdiff
|
raw
|
diff to current
2020-07-14
Andrew Reynolds
Remove sygus print callback (#4727)
blob
|
commitdiff
|
raw
|
diff to current
2020-07-14
Andrew Reynolds
(proof-new) Skeleton proof support in the Rewriter...
blob
|
commitdiff
|
raw
|
diff to current
2020-07-13
Andrew Reynolds
(proof-new) SMT Preprocess proof generator (#4708)
blob
|
commitdiff
|
raw
|
diff to current
2020-07-13
Andres Noetzli
Remove ExprSequence (#4724)
blob
|
commitdiff
|
raw
|
diff to current
2020-07-10
Ying Sheng
[Interpolation] Add interface for SyGuS interpolation...
blob
|
commitdiff
|
raw
|
diff to current
2020-07-09
Andrew Reynolds
Associate all lemmas in non-linear arithmetic with...
blob
|
commitdiff
|
raw
|
diff to current
2020-07-09
Andrew Reynolds
(proof-new) Theory engine proof generator (#4657)
blob
|
commitdiff
|
raw
|
diff to current
2020-07-02
Andrew Reynolds
(proof-new) Proof rule checkers run on skolem forms...
blob
|
commitdiff
|
raw
|
diff to current
2020-07-01
Andrew Reynolds
Add solver for integer AND (#4681)
blob
|
commitdiff
|
raw
|
diff to current
2020-06-30
Andrew Reynolds
Add internal support for integer and operator (#4668)
blob
|
commitdiff
|
raw
|
diff to current
2020-06-19
Andrew Reynolds
(proof-new) Split operator elimination from arithmetic...
blob
|
commitdiff
|
raw
|
diff to current
2020-06-19
Andrew Reynolds
Clean the header file of TheoryStrings (#4272)
blob
|
commitdiff
|
raw
|
diff to current
2020-06-16
Andrew Reynolds
(proof-new) Add quantifiers proof checker (#4593)
blob
|
commitdiff
|
raw
|
diff to current
2020-06-13
Andrew Reynolds
Move sygus datatype utility functions to their own...
blob
|
commitdiff
|
raw
|
diff to current
2020-06-12
Andrew Reynolds
(proof-new) Split TheoryEngine (#4558)
blob
|
commitdiff
|
raw
|
diff to current
2020-06-11
Andrew Reynolds
(proof-new) Add eager proof generator utility. (#4592)
blob
|
commitdiff
|
raw
|
diff to current
2020-06-10
Andrew Reynolds
(proof-new) Theory proof step buffer utility (#4580)
blob
|
commitdiff
|
raw
|
diff to current
2020-06-09
Andrew Reynolds
(proof-new) Add trust node utility (#4588)
blob
|
commitdiff
|
raw
|
diff to current
2020-06-03
Haniel Barbosa
(proof-new) Adding rules and proof checker for EUF...
blob
|
commitdiff
|
raw
|
diff to current
2020-06-03
Haniel Barbosa
(proof-new) Adding rules and proof checker for Boolean...
blob
|
commitdiff
|
raw
|
diff to current
2020-06-03
Andrew Reynolds
(proof-new) Add builtin proof checker (#4537)
blob
|
commitdiff
|
raw
|
diff to current
2020-06-01
Andrew Reynolds
Move non-linear files to src/theory/arith/nl (#4548)
blob
|
commitdiff
|
raw
|
diff to current
2020-05-27
Andrew Reynolds
Add the Expr-level sequence datatype (#4526)
blob
|
commitdiff
|
raw
|
diff to current
2020-05-22
Aina Niemetz
Add support for SAT solver Kissat. (#4514)
blob
|
commitdiff
|
raw
|
diff to current
2020-04-17
Mathias Preiner
SyGuS instantiation quantifiers module (#3910)
blob
|
commitdiff
|
raw
|
diff to current
2020-04-15
Andrew Reynolds
Split TermRegistry object from TheoryStrings (#4312)
blob
|
commitdiff
|
raw
|
diff to current
2020-04-14
Andrew Reynolds
Remove argument extender (#4223)
blob
|
commitdiff
|
raw
|
diff to current
2020-04-11
Andrew Reynolds
Split the non-linear solver (#4219)
blob
|
commitdiff
|
raw
|
diff to current
2020-04-09
Andrew Reynolds
Split ProcessAssertions module from SmtEngine (#4210)
blob
|
commitdiff
|
raw
|
diff to current
2020-04-03
Andrew Reynolds
Split sequences rewriter (#4194)
blob
|
commitdiff
|
raw
|
diff to current
2020-03-31
Andrew Reynolds
Remove replay and use-theory options and idl (#4186)
blob
|
commitdiff
|
raw
|
diff to current
2020-03-30
Andrew Reynolds
Support indexed operators re.loop and re.^ (#4167)
blob
|
commitdiff
|
raw
|
diff to current
2020-03-29
Andrew Reynolds
Enumeration for String rewrites (#4173)
blob
|
commitdiff
|
raw
|
diff to current
2020-03-28
Andrew Reynolds
Split transcendental solver to its own file (#4156)
blob
|
commitdiff
|
raw
|
diff to current
2020-03-27
Andrew Reynolds
Move string utility file (#4164)
blob
|
commitdiff
|
raw
|
diff to current
2020-03-27
Andrew Reynolds
Move set defaults function to its own file (#4154)
blob
|
commitdiff
|
raw
|
diff to current
2020-03-23
Andres Noetzli
Collect statistics about normal form inferences (#4127)
blob
|
commitdiff
|
raw
|
diff to current
2020-03-20
Andrew Reynolds
Split string-specific operators from TheoryStringsRewri...
blob
|
commitdiff
|
raw
|
diff to current
2020-03-20
Andrew Reynolds
Refactor enumerator for strings (#4014)
blob
|
commitdiff
|
raw
|
diff to current
2020-03-18
Alex Ozdemir
Move node visitor class from smt_util/ to expr/ (#4110)
blob
|
commitdiff
|
raw
|
diff to current
2020-03-11
Andrew Reynolds
Remove experimental symmetry breaker (#4005)
blob
|
commitdiff
|
raw
|
diff to current
2020-03-11
Andrew Reynolds
Remove partial instantiation for local theory extension...
blob
|
commitdiff
|
raw
|
diff to current
2020-03-10
Andrew Reynolds
Remove instantiation propagator infrastructure (#3975)
blob
|
commitdiff
|
raw
|
diff to current
2020-03-06
Andres Noetzli
Remove --apply-to-const preprocessing pass (#3919)
blob
|
commitdiff
|
raw
|
diff to current
2020-03-03
mudathirmahgoub
Refactoring and cleaning the type enumerator for sets...
blob
|
commitdiff
|
raw
|
diff to current
2020-03-03
Andrew Reynolds
Standardize the interface for SMT engine subsolvers...
blob
|
commitdiff
|
raw
|
diff to current
2020-02-26
Andrew Reynolds
Use side effect utility for non-linear lemmas (#3780)
blob
|
commitdiff
|
raw
|
diff to current
2020-02-26
Andrew Reynolds
Move equivalence class info to its own file in strings...
blob
|
commitdiff
|
raw
|
diff to current
2020-02-26
Andres Noetzli
Remove portfolio leftovers (#3821)
blob
|
commitdiff
|
raw
|
diff to current
2020-02-25
yoni206
bv_to_int preprocessing pass
blob
|
commitdiff
|
raw
|
diff to current
2020-02-24
Andrew Reynolds
Utilities for words (#3797)
blob
|
commitdiff
|
raw
|
diff to current
2020-02-21
Andrew Reynolds
Split extended functions solver in strings (#3768)
blob
|
commitdiff
|
raw
|
diff to current
2020-02-20
Andrew Reynolds
Remove front-end support for Chain (#3767)
blob
|
commitdiff
|
raw
|
diff to current
2020-02-14
Andrew Reynolds
Remove quantifiers rewrite rules infrastructure (#3754)
blob
|
commitdiff
|
raw
|
diff to current
2020-02-14
Andrew Reynolds
Update sygus v1 parser to use ParseOp utility (#3756)
blob
|
commitdiff
|
raw
|
diff to current
2020-02-08
Andrew Reynolds
Split strings finite model finding strategy (#3727)
blob
|
commitdiff
|
raw
|
diff to current
2020-02-08
Andrew Reynolds
Split core solver from the theory of strings (#3713)
blob
|
commitdiff
|
raw
|
diff to current
2020-02-08
Andrew Reynolds
Interface for example evaluation cache utilities (...
blob
|
commitdiff
|
raw
|
diff to current
2020-02-04
Andrew Reynolds
Split base solver from the theory of strings (#3680)
blob
|
commitdiff
|
raw
|
diff to current
2020-02-03
Andrew Reynolds
Example inference utility (#3670)
blob
|
commitdiff
|
raw
|
diff to current
2020-01-31
Andrew Reynolds
Refactor sygus stats (#3684)
blob
|
commitdiff
|
raw
|
diff to current
2020-01-30
Andrew Reynolds
Example minimize evaluation utility. (#3671)
blob
|
commitdiff
|
raw
|
diff to current
2019-12-17
Mathias Preiner
Generate code for options with modes. (#3561)
blob
|
commitdiff
|
raw
|
diff to current
2019-12-09
Andres Noetzli
Make theory rewriters non-static (#3547)
blob
|
commitdiff
|
raw
|
diff to current
2019-12-06
Andrew Reynolds
New algorithm for interpolation and abduction based...
blob
|
commitdiff
|
raw
|
diff to current
2019-11-06
Andrew Reynolds
Support for SyGuS PBE + recursive functions (#3433)
blob
|
commitdiff
|
raw
|
diff to current
2019-11-05
Andrew Reynolds
Separate model object in non-linear extension (#3426)
blob
|
commitdiff
|
raw
|
diff to current
2019-11-01
Andrew Reynolds
Rename datatypes sygus solver (#3417)
blob
|
commitdiff
|
raw
|
diff to current
2019-10-30
Andrew Reynolds
Split some generic utilities from the non-linear extens...
blob
|
commitdiff
|
raw
|
diff to current
2019-10-17
Andrew Reynolds
Move datatype utility functions to own file (#3397)
blob
|
commitdiff
|
raw
|
diff to current
2019-10-16
Andrew Reynolds
Solver state for theory of strings (#3181)
blob
|
commitdiff
|
raw
|
diff to current
2019-10-11
Aina Niemetz
Make order of theories explicit in the source code...
blob
|
commitdiff
|
raw
|
diff to current
2019-10-08
Ying Sheng
Make ackermannization generally applicable rather than...
blob
|
commitdiff
|
raw
|
diff to current
2019-09-25
Mathias Preiner
Use separate CMake project for CVC4 examples. (#3196)
blob
|
commitdiff
|
raw
|
diff to current
2019-09-16
Andrew Reynolds
Sygus type info class (#3187)
blob
|
commitdiff
|
raw
|
diff to current
2019-09-16
Andrew Reynolds
Move virtual term substitution utilities to own file...
blob
|
commitdiff
|
raw
|
diff to current
2019-09-13
Andrew Reynolds
Split, refactor and document the theory of sets (#3085)
blob
|
commitdiff
|
raw
|
diff to current
2019-09-12
Andrew Reynolds
Rename UF with cardinality extension (#3241)
blob
|
commitdiff
|
raw
|
diff to current
2019-09-12
Andrew Reynolds
Refactoring finite bounds in Quantifiers Engine (#3261)
blob
|
commitdiff
|
raw
|
diff to current
2019-09-07
Andrew Reynolds
Remove portfolio (#3236)
blob
|
commitdiff
|
raw
|
diff to current
2019-08-23
Andrew Reynolds
Document transition inference utility (#3207)
blob
|
commitdiff
|
raw
|
diff to current
2019-08-14
Mathias Preiner
cmake: Export CVC4 library interface. (#3179)
blob
|
commitdiff
|
raw
|
diff to current
2019-08-02
Andrew Reynolds
Move basic sygus enumerator to its own file (#3149)
blob
|
commitdiff
|
raw
|
diff to current
2019-08-01
Andrew Reynolds
Move some generic utilities out of quantifiers (#3139)
blob
|
commitdiff
|
raw
|
diff to current
2019-07-29
Andrew Reynolds
Model blocker feature (#3112)
blob
|
commitdiff
|
raw
|
diff to current
2019-07-29
Andrew Reynolds
Support get-abduct smt2 command (#3122)
blob
|
commitdiff
|
raw
|
diff to current
2019-07-25
Andrew Reynolds
Split infer info data structure in strings (#3107)
blob
|
commitdiff
|
raw
|
diff to current
2019-07-08
Andrew Reynolds
Towards refactoring relations (#3078)
blob
|
commitdiff
|
raw
|
diff to current
next