projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Refactoring of proof manager initialization (#7073)
2021-09-07
Andrew Reynolds
Refactoring of proof manager initialization (#7073)
commit
|
commitdiff
|
tree
2021-09-07
Andrew Reynolds
Refactoring and fixes of set defaults for quantifiers...
commit
|
commitdiff
|
tree
2021-09-03
Andrew Reynolds
Standardize Rewriter::rewriteViaMethod call (#7119)
commit
|
commitdiff
|
tree
2021-09-03
Andrew Reynolds
Make quantifier module classes derive from EnvObj ...
commit
|
commitdiff
|
tree
2021-09-03
Andrew Reynolds
Eliminate backwards ref to SmtEngine from abduction...
commit
|
commitdiff
|
tree
2021-09-02
Andrew Reynolds
Add LFSC node converter (#6944)
commit
|
commitdiff
|
tree
2021-09-02
Andrew Reynolds
Remove more instances of ufHo (#7087)
commit
|
commitdiff
|
tree
2021-09-02
Andrew Reynolds
Implement lazy proof checking modes (#7106)
commit
|
commitdiff
|
tree
2021-09-01
Andrew Reynolds
Print response to get-model using the API (#7084)
commit
|
commitdiff
|
tree
2021-09-01
Andrew Reynolds
Fix issues with cyclic proofs due to double SYMM application...
commit
|
commitdiff
|
tree
2021-09-01
Andrew Reynolds
Lazy proof reconstruction for strings theory solver...
commit
|
commitdiff
|
tree
2021-08-31
Andrew Reynolds
Fix normal forms context-dependent simplification for...
commit
|
commitdiff
|
tree
2021-08-31
Andrew Reynolds
Make regular expression sort not closed enumerable...
commit
|
commitdiff
|
tree
2021-08-30
Andrew Reynolds
Further refactoring of set defaults for incompatibility...
commit
|
commitdiff
|
tree
2021-08-30
Andrew Reynolds
Fix proof equality engine for "no-explain" premises...
commit
|
commitdiff
|
tree
2021-08-30
Andrew Reynolds
Fix quantifiers dynamic split module for parametric...
commit
|
commitdiff
|
tree
2021-08-27
Andrew Reynolds
Expand definitions in sygus operators at the SMT level...
commit
|
commitdiff
|
tree
2021-08-27
Andrew Reynolds
Add n-ary match trie utility (#6909)
commit
|
commitdiff
|
tree
2021-08-27
Andrew Reynolds
Add missing methods to Solver API for models (#7052)
commit
|
commitdiff
|
tree
2021-08-26
Andrew Reynolds
Eliminate currentSmtEngine for subsolver calls (#7068)
commit
|
commitdiff
|
tree
2021-08-26
Andrew Reynolds
Dump models for isNotEntailed results (#7071)
commit
|
commitdiff
|
tree
2021-08-26
Andrew Reynolds
Make datatype selector expansion to its own accessible...
commit
|
commitdiff
|
tree
2021-08-25
Andrew Reynolds
Eliminate calls to currentSmtEngine (#7060)
commit
|
commitdiff
|
tree
2021-08-24
Andrew Reynolds
Split higher-order term database (#7045)
commit
|
commitdiff
|
tree
2021-08-24
Andrew Reynolds
Refactor enumerator management in synth conjecture...
commit
|
commitdiff
|
tree
2021-08-24
Andrew Reynolds
Top-level structure for set defaults (#7047)
commit
|
commitdiff
|
tree
2021-08-24
Andrew Reynolds
Uniform treatment of trusted theory inferences in proofs...
commit
|
commitdiff
|
tree
2021-08-24
Andrew Reynolds
Miscellaneous changes from proof-new (#7042)
commit
|
commitdiff
|
tree
2021-08-23
Andrew Reynolds
Fix non-deterministism in quantified datatypes expansion...
commit
|
commitdiff
|
tree
2021-08-23
Andrew Reynolds
Purify substitutions in strings proof reconstruction...
commit
|
commitdiff
|
tree
2021-08-23
Andrew Reynolds
Generalize inequality elimination in quantifiers rewriter...
commit
|
commitdiff
|
tree
2021-08-23
Andrew Reynolds
Fix single invocation partition for higher-order (...
commit
|
commitdiff
|
tree
2021-08-22
Andrew Reynolds
Simplify model printing modes (#7049)
commit
|
commitdiff
|
tree
2021-08-22
Andrew Reynolds
Prenex quantified formulas with user annotations by...
commit
|
commitdiff
|
tree
2021-08-20
Andrew Reynolds
Simplify how user-provided quantifier attributes are...
commit
|
commitdiff
|
tree
2021-08-20
Andrew Reynolds
More refactoring of set defaults (#7043)
commit
|
commitdiff
|
tree
2021-08-20
Andrew Reynolds
Support sygus standard command syntax set-feature ...
commit
|
commitdiff
|
tree
2021-08-20
Andrew Reynolds
Eliminate eager model building (#7038)
commit
|
commitdiff
|
tree
2021-08-19
Andrew Reynolds
Catch cases where recursive functions reference functions...
commit
|
commitdiff
|
tree
2021-08-19
Andrew Reynolds
Split proof final callback to its own file (#6984)
commit
|
commitdiff
|
tree
2021-08-19
Andrew Reynolds
Refactor proof output for TPTP (#7029)
commit
|
commitdiff
|
tree
2021-08-18
Andrew Reynolds
Make TheoryProxy use Env, simplify initialization of...
commit
|
commitdiff
|
tree
2021-08-17
Andrew Reynolds
Make SmtEngineState use Env (#7028)
commit
|
commitdiff
|
tree
2021-08-17
Andrew Reynolds
Refactoring theory-specific variable elimination in...
commit
|
commitdiff
|
tree
2021-08-17
Andrew Reynolds
Fix policy for eliminating quantified formulas (#7017)
commit
|
commitdiff
|
tree
2021-08-17
Andrew Reynolds
Make theory BV use central eq engine when option is...
commit
|
commitdiff
|
tree
2021-08-17
Andrew Reynolds
Cosmetic improvements to theory datatypes (#7020)
commit
|
commitdiff
|
tree
2021-08-17
Andrew Reynolds
Improve conversion to skolems in expression miner ...
commit
|
commitdiff
|
tree
2021-08-17
Andrew Reynolds
Initial refactoring of set defaults (#7021)
commit
|
commitdiff
|
tree
2021-08-05
Andrew Reynolds
Generalize term canonizer for type classes (#6895)
commit
|
commitdiff
|
tree
2021-08-05
Andrew Reynolds
Fix policy for rewriting string equalities (#6916)
commit
|
commitdiff
|
tree
2021-08-04
Andrew Reynolds
Proper printing of proofs in the internal calculus...
commit
|
commitdiff
|
tree
2021-08-04
Andrew Reynolds
Fix policy for merging subproofs (#6981)
commit
|
commitdiff
|
tree
2021-08-04
Andrew Reynolds
Add inference ids for remainder of sygus solver (#6977)
commit
|
commitdiff
|
tree
2021-08-04
Andrew Reynolds
Add optional debug information for dumping instantiations...
commit
|
commitdiff
|
tree
2021-08-04
Andrew Reynolds
Add containsAssumption proof utility (#6953)
commit
|
commitdiff
|
tree
2021-08-04
Andrew Reynolds
Add missing inference identifiers (#6962)
commit
|
commitdiff
|
tree
2021-08-04
Andrew Reynolds
Remove dependencies on smt engine in smt solver (#6965)
commit
|
commitdiff
|
tree
2021-08-03
Andrew Reynolds
Refactor shared solver to use theory builtin inference...
commit
|
commitdiff
|
tree
2021-08-03
Andrew Reynolds
Remove "inUnsatCore" flag throughout (#6964)
commit
|
commitdiff
|
tree
2021-07-30
Andrew Reynolds
Simplify smt2 printer (#6954)
commit
|
commitdiff
|
tree
2021-07-29
Andrew Reynolds
Integrate central equality engine approach into theory...
commit
|
commitdiff
|
tree
2021-07-29
Andrew Reynolds
Minor updates to shared terms database for central...
commit
|
commitdiff
|
tree
2021-07-28
Andrew Reynolds
Minor changes to arrays in preparation for central...
commit
|
commitdiff
|
tree
2021-07-28
Andrew Reynolds
Make extended rewriter methods const (#6948)
commit
|
commitdiff
|
tree
2021-07-27
Andrew Reynolds
Track instantiation reasons in proofs (#6935)
commit
|
commitdiff
|
tree
2021-07-27
Andrew Reynolds
Add basic LFSC utilities (#6879)
commit
|
commitdiff
|
tree
2021-07-27
Andrew Reynolds
Move enum value generator to own file (#6941)
commit
|
commitdiff
|
tree
2021-07-27
Andrew Reynolds
Minor fix for term database + central equality engine...
commit
|
commitdiff
|
tree
2021-07-27
Andrew Reynolds
Revert change to regression (#6940)
commit
|
commitdiff
|
tree
2021-07-27
Andrew Reynolds
Make all dependencies in the fast enumerator optional...
commit
|
commitdiff
|
tree
2021-07-27
Andrew Reynolds
Add print expression utility (#6880)
commit
|
commitdiff
|
tree
2021-07-27
Andrew Reynolds
Minor changes from proof-new (#6937)
commit
|
commitdiff
|
tree
2021-07-27
Andrew Reynolds
Miscellaneous fixes from proof-new (#6914)
commit
|
commitdiff
|
tree
2021-07-27
Andrew Reynolds
Add proof letify utility (#6881)
commit
|
commitdiff
|
tree
2021-07-27
Andrew Reynolds
Fix eq proof conversion for constant merged parameterized...
commit
|
commitdiff
|
tree
2021-07-27
Andrew Reynolds
Default equality proofs for bags and separation logic...
commit
|
commitdiff
|
tree
2021-07-27
Andrew Reynolds
Add sygus enumerator callback (#6923)
commit
|
commitdiff
|
tree
2021-07-26
Andrew Reynolds
Enable default equality proofs for sets (#6931)
commit
|
commitdiff
|
tree
2021-07-26
Andrew Reynolds
More updates to arithmetic in preparation for central...
commit
|
commitdiff
|
tree
2021-07-25
Andrew Reynolds
Changes to datatypes in preparation for central equality...
commit
|
commitdiff
|
tree
2021-07-25
Andrew Reynolds
Refactor equality engine setup for arithmetic congruence...
commit
|
commitdiff
|
tree
2021-07-22
Andrew Reynolds
Simplify computation of relevant terms in datatypes...
commit
|
commitdiff
|
tree
2021-07-22
Andrew Reynolds
Add the central equality engine manager (#6893)
commit
|
commitdiff
|
tree
2021-07-22
Andrew Reynolds
Miscellaneous changes in preparation for central equality...
commit
|
commitdiff
|
tree
2021-07-22
Andrew Reynolds
Preparation for carry the rewrite rule database in...
commit
|
commitdiff
|
tree
2021-07-18
Andrew Reynolds
Add n-ary term utilities (#6896)
commit
|
commitdiff
|
tree
2021-07-16
Andrew Reynolds
Do not exhaustive instantiation when FMF is disabled...
commit
|
commitdiff
|
tree
2021-07-15
Andrew Reynolds
Fix context for proofs of instantiations (#6890)
commit
|
commitdiff
|
tree
2021-07-15
Andrew Reynolds
Distinguish quantifiers preprocess as its own proof...
commit
|
commitdiff
|
tree
2021-07-15
Andrew Reynolds
Connect the equality solver to theory arith (#6894)
commit
|
commitdiff
|
tree
2021-07-15
Andrew Reynolds
Arithmetic equality solver (#6876)
commit
|
commitdiff
|
tree
2021-07-15
Andrew Reynolds
Move master equality engine notification to own file...
commit
|
commitdiff
|
tree
2021-07-15
Andrew Reynolds
Add node converter utility (#6878)
commit
|
commitdiff
|
tree
2021-07-14
Andrew Reynolds
Fix for context on input proof generator (#6873)
commit
|
commitdiff
|
tree
2021-07-14
Andrew Reynolds
Move synthesis verification check to own file (#6882)
commit
|
commitdiff
|
tree
2021-07-14
Andrew Reynolds
Refactor setup of proof equality engine for central...
commit
|
commitdiff
|
tree
2021-07-14
Andrew Reynolds
Fix models for sequences of infinite element type ...
commit
|
commitdiff
|
tree
2021-07-13
Andrew Reynolds
Add branch and bound lemma if linear arithmetic generates...
commit
|
commitdiff
|
tree
2021-07-12
Andrew Reynolds
Add branch and bound (#6865)
commit
|
commitdiff
|
tree
next