projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Add TheoryInference base class (#4990)
[cvc5.git]
/
src
/
CMakeLists.txt
2020-09-01
Andrew Reynolds
Add TheoryInference base class (#4990)
blob
|
commitdiff
|
raw
2020-09-01
Andrew Reynolds
Add the inference manager for datatypes (#4968)
blob
|
commitdiff
|
raw
|
diff to current
2020-08-28
Andrew Reynolds
Add the buffered inference manager (#4954)
blob
|
commitdiff
|
raw
|
diff to current
2020-08-27
Andrew Reynolds
(proof-new) Add the proof equality engine (#4881)
blob
|
commitdiff
|
raw
|
diff to current
2020-08-27
Andrew Reynolds
Add the theory inference manager (#4948)
blob
|
commitdiff
|
raw
|
diff to current
2020-08-26
Andrew Reynolds
Replace Expr-level datatype with Node-level DType ...
blob
|
commitdiff
|
raw
|
diff to current
2020-08-25
Andrew Reynolds
Add the combination engine (#4939)
blob
|
commitdiff
|
raw
|
diff to current
2020-08-24
Andrew Reynolds
Add the distributed model manager (#4934)
blob
|
commitdiff
|
raw
|
diff to current
2020-08-21
Andrew Reynolds
Dynamic allocation of model equality engine (#4911)
blob
|
commitdiff
|
raw
|
diff to current
2020-08-20
Andrew Reynolds
Add TheoryState objects to each Theory (#4920)
blob
|
commitdiff
|
raw
|
diff to current
2020-08-20
Andrew Reynolds
Split QuantElimSolver from SmtEngine (#4919)
blob
|
commitdiff
|
raw
|
diff to current
2020-08-18
Andrew Reynolds
Introduce the theory state object (#4910)
blob
|
commitdiff
|
raw
|
diff to current
2020-08-18
Andrew Reynolds
Split SygusSolver from SmtEngine (#4891)
blob
|
commitdiff
|
raw
|
diff to current
2020-08-18
Andrew Reynolds
Add the relevance manager module (#4894)
blob
|
commitdiff
|
raw
|
diff to current
2020-08-15
Andrew Reynolds
(proof-new) Add the strings proof checker (#4858)
blob
|
commitdiff
|
raw
|
diff to current
2020-08-13
Andrew Reynolds
Split SmtSolver from SmtEngine (#4880)
blob
|
commitdiff
|
raw
|
diff to current
2020-08-13
Andrew Reynolds
Add the distributed equality engine manager (#4867)
blob
|
commitdiff
|
raw
|
diff to current
2020-08-12
makaimann
Add option to only build library (#4801)
blob
|
commitdiff
|
raw
|
diff to current
2020-08-12
Andrew Reynolds
(proof-new) Witness form proof generator (#4782)
blob
|
commitdiff
|
raw
|
diff to current
2020-08-12
Andrew Reynolds
Split SmtEngineState from SmtEngine (#4855)
blob
|
commitdiff
|
raw
|
diff to current
2020-08-09
Andrew Reynolds
Splitting a few utility classes from EqualityEngine...
blob
|
commitdiff
|
raw
|
diff to current
2020-08-06
Andrew Reynolds
Split preprocessor from SmtEngine (#4854)
blob
|
commitdiff
|
raw
|
diff to current
2020-08-05
Andrew Reynolds
Split Assertions from SmtEngine (#4788)
blob
|
commitdiff
|
raw
|
diff to current
2020-08-04
Gereon Kremer
Add CAD-based solver (#4834)
blob
|
commitdiff
|
raw
|
diff to current
2020-08-03
Andrew Reynolds
Split expression names from SmtEngine (#4832)
blob
|
commitdiff
|
raw
|
diff to current
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
next