projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Require ITE branches to be first class types (#7508)
2021-10-27
Andrew Reynolds
Fix care graph computation for higher-order (#7474)
commit
|
commitdiff
|
tree
2021-10-27
Andrew Reynolds
Fix model unsoundness for relation join (#7511)
commit
|
commitdiff
|
tree
2021-10-27
Andrew Reynolds
Avoid non-terminating check with assumptions in strings...
commit
|
commitdiff
|
tree
2021-10-27
Andrew Reynolds
Deterministic variables for RE elim (#7489)
commit
|
commitdiff
|
tree
2021-10-26
Andrew Reynolds
Disable automatic symmetry in proofs of theory explanations...
commit
|
commitdiff
|
tree
2021-10-26
Andrew Reynolds
Add regressions for fixed issues (#7495)
commit
|
commitdiff
|
tree
2021-10-26
Andrew Reynolds
Disable sygus-inst when incremental (#7485)
commit
|
commitdiff
|
tree
2021-10-25
Andrew Reynolds
Add new method for enumerating unsat queries with SyGuS...
commit
|
commitdiff
|
tree
2021-10-25
Andrew Reynolds
Fix spurious checks to closed proofs (#7484)
commit
|
commitdiff
|
tree
2021-10-25
Andrew Reynolds
Java and python unit tests for mkCardinalityConstraint...
commit
|
commitdiff
|
tree
2021-10-25
Andrew Reynolds
Fix more missing uses of CDProof::isSame (#7491)
commit
|
commitdiff
|
tree
2021-10-25
Andrew Reynolds
Fix support for global declarations (#7480)
commit
|
commitdiff
|
tree
2021-10-25
Andrew Reynolds
Remove HOL/fmf bound messages in set defaults (#7487)
commit
|
commitdiff
|
tree
2021-10-25
Andrew Reynolds
Reenable proofs on some regressions (#7483)
commit
|
commitdiff
|
tree
2021-10-24
Andrew Reynolds
Add new eager conflict detection in strings for integer...
commit
|
commitdiff
|
tree
2021-10-23
Andrew Reynolds
Remove spurious assertoin (#7458)
commit
|
commitdiff
|
tree
2021-10-22
Andrew Reynolds
Add requires libpoly to regression (#7467)
commit
|
commitdiff
|
tree
2021-10-22
Andrew Reynolds
Remove stale pointer to proof node manager from skolemize...
commit
|
commitdiff
|
tree
2021-10-22
Andrew Reynolds
Remove `--uf-ho` option (#7463)
commit
|
commitdiff
|
tree
2021-10-22
Andrew Reynolds
Fix symmetry issue in theory engine conflicts (#7469)
commit
|
commitdiff
|
tree
2021-10-22
Andrew Reynolds
Add more abduction regressions (#7461)
commit
|
commitdiff
|
tree
2021-10-22
Andrew Reynolds
Refactor theory inference manager constructor (#7457)
commit
|
commitdiff
|
tree
2021-10-22
Andrew Reynolds
Do not use global proxy variable attribute for strings...
commit
|
commitdiff
|
tree
2021-10-22
Andrew Reynolds
Make expression mining use configurable options and...
commit
|
commitdiff
|
tree
2021-10-21
Andrew Reynolds
Split utilites from CEGIS core connective module (...
commit
|
commitdiff
|
tree
2021-10-21
Andrew Reynolds
Make cardinality constraint a nullary operator (#7333)
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Enable some previously failing regressions (#7434)
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Move variadic trie utility to its own file (#7410)
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Add regressions for fixed issues (#7421)
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Throw exception if checking model with separation logic...
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Check for higher-order variables in TheoryUF::ppRewrite...
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Eliminate last static calls to rewriter from smt layer...
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Make SyGuS solver robust to non-closed enumerable sorts...
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Do not construct instantiation for checking propagating...
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Check whether abduct option is enabled (#7418)
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Add LFSC signature for n-ary programs (#7360)
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Use codatatype bound variables for codatatype values...
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Reimplement support for relational triggers (#7063)
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Do not make assumption about model for Boolean variables...
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Correctly parse uninterpreted constant values in get...
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Make proofs of rewrites robust to use in internal subsolvers...
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Add basic regular expression type enumerator (#7416)
commit
|
commitdiff
|
tree
2021-10-19
Andrew Reynolds
Fix expected conclusion for EQ_RESOLVE when expanding...
commit
|
commitdiff
|
tree
2021-10-19
Andrew Reynolds
Support sequences of fixed finite cardinality (#7371)
commit
|
commitdiff
|
tree
2021-10-19
Andrew Reynolds
Fix issue related to sanity checking integer models...
commit
|
commitdiff
|
tree
2021-10-18
Andrew Reynolds
Add regression for fixed issue (#7395)
commit
|
commitdiff
|
tree
2021-10-15
Andrew Reynolds
Add more regressions for fixed issues (#7382)
commit
|
commitdiff
|
tree
2021-10-15
Andrew Reynolds
Fix issues related to proofs of lemmas with duplicate...
commit
|
commitdiff
|
tree
2021-10-14
Andrew Reynolds
Add regressions for fixed issues (#7369)
commit
|
commitdiff
|
tree
2021-10-14
Andrew Reynolds
Add regression for fixed issue (#7365)
commit
|
commitdiff
|
tree
2021-10-14
Andrew Reynolds
Improve parser for tuple select (#7364)
commit
|
commitdiff
|
tree
2021-10-14
Andrew Reynolds
Split entailment check from term database (#7342)
commit
|
commitdiff
|
tree
2021-10-14
Andrew Reynolds
Fix quantifiers variable elimination for parametric...
commit
|
commitdiff
|
tree
2021-10-14
Andrew Reynolds
Add core LFSC signatures (#7289)
commit
|
commitdiff
|
tree
2021-10-13
Andrew Reynolds
Eliminate uses of rewrite from datatypes theory (#7354)
commit
|
commitdiff
|
tree
2021-10-13
Andrew Reynolds
Make (proof) equality engine use Env (#7336)
commit
|
commitdiff
|
tree
2021-10-12
Andrew Reynolds
Simplify refinement in sygus solver (#7343)
commit
|
commitdiff
|
tree
2021-10-12
Andrew Reynolds
Eliminate calls to currentResourceManager (#7350)
commit
|
commitdiff
|
tree
2021-10-12
Andrew Reynolds
Provide a non-traversal interface to term formula removal...
commit
|
commitdiff
|
tree
2021-10-12
Andrew Reynolds
Minor cleaning of instantiation utilities (#7334)
commit
|
commitdiff
|
tree
2021-10-12
Andrew Reynolds
Simplify skolemization in sygus solver (#7331)
commit
|
commitdiff
|
tree
2021-10-11
Andrew Reynolds
Connect the LFSC printer (#7323)
commit
|
commitdiff
|
tree
2021-10-11
Andrew Reynolds
Add cardinality constraint utilities (#7286)
commit
|
commitdiff
|
tree
2021-10-08
Andrew Reynolds
Make skolem definition manager robust to function skolems...
commit
|
commitdiff
|
tree
2021-10-08
Andrew Reynolds
Add argument to distinguish lemmas and input assertions...
commit
|
commitdiff
|
tree
2021-10-08
Andrew Reynolds
A few more miscellaneous uses of EnvObj (#7325)
commit
|
commitdiff
|
tree
2021-10-07
Andrew Reynolds
Move preprocessor to smt solver (#7321)
commit
|
commitdiff
|
tree
2021-10-07
Andrew Reynolds
Finish the LFSC printer (#7285)
commit
|
commitdiff
|
tree
2021-10-07
Andrew Reynolds
Use skolem lemma in prop layer interfaces (#7320)
commit
|
commitdiff
|
tree
2021-10-07
Andrew Reynolds
Make the cardinality of the alphabet of strings configurable...
commit
|
commitdiff
|
tree
2021-10-07
Andrew Reynolds
Miscellaneous fixes from proof-new (#7313)
commit
|
commitdiff
|
tree
2021-10-07
Andrew Reynolds
Fast exit for string extended equality rewriter (#7312)
commit
|
commitdiff
|
tree
2021-10-07
Andrew Reynolds
Eliminate more circular dependencies on solver engine...
commit
|
commitdiff
|
tree
2021-10-06
Andrew Reynolds
Refactor skolem definitions notifications for the decision...
commit
|
commitdiff
|
tree
2021-10-06
Andrew Reynolds
Eliminate more hard coded uses of user context (#7309)
commit
|
commitdiff
|
tree
2021-10-04
Andrew Reynolds
Refactor internally generated bounded quantified formulas...
commit
|
commitdiff
|
tree
2021-10-04
Andrew Reynolds
Move isFiniteType from theory engine to Env (#7287)
commit
|
commitdiff
|
tree
2021-10-04
Andrew Reynolds
Make decision engine use env (#7300)
commit
|
commitdiff
|
tree
2021-10-04
Andrew Reynolds
Eliminating static calls to rewriter in quantifiers...
commit
|
commitdiff
|
tree
2021-10-04
Andrew Reynolds
Eliminating static calls to rewriter from strings ...
commit
|
commitdiff
|
tree
2021-10-01
Andrew Reynolds
Update theory preprocessor to use Env (#7288)
commit
|
commitdiff
|
tree
2021-10-01
Andrew Reynolds
Fix ascription check for return types on ordinary functions...
commit
|
commitdiff
|
tree
2021-10-01
Andrew Reynolds
Make preregistration safe for uninterpreted constants...
commit
|
commitdiff
|
tree
2021-10-01
Andrew Reynolds
Add the LFSC printer (#7158)
commit
|
commitdiff
|
tree
2021-10-01
Andrew Reynolds
Add the print benchmark utility (#7196)
commit
|
commitdiff
|
tree
2021-10-01
Andrew Reynolds
Use the proper evaluator for optimized SyGuS datatype...
commit
|
commitdiff
|
tree
2021-09-30
Andrew Reynolds
Make theory engine modules use Env (#7277)
commit
|
commitdiff
|
tree
2021-09-30
Andrew Reynolds
Simplify the syntax and representation of the separation...
commit
|
commitdiff
|
tree
2021-09-29
Andrew Reynolds
Properly restrict PBE symmetry breaking for abduction...
commit
|
commitdiff
|
tree
2021-09-29
Andrew Reynolds
Update the syntax for tuples in smt2 (#7265)
commit
|
commitdiff
|
tree
2021-09-29
Andrew Reynolds
Add the strings array solver (#7232)
commit
|
commitdiff
|
tree
2021-09-24
Andrew Reynolds
Eliminate calls to Rewriter::rewrite from strings entailment...
commit
|
commitdiff
|
tree
2021-09-23
Andrew Reynolds
Generalize string enumerator for fixed length sequences...
commit
|
commitdiff
|
tree
2021-09-23
Andrew Reynolds
More uses of EnvObj (#7230)
commit
|
commitdiff
|
tree
2021-09-23
Andrew Reynolds
Implement alpha equivalence proofs (#7066)
commit
|
commitdiff
|
tree
2021-09-22
Andrew Reynolds
Make cegqi subsolvers EnvObj (#7205)
commit
|
commitdiff
|
tree
2021-09-22
Andrew Reynolds
Towards standard usage of evaluator (#7189)
commit
|
commitdiff
|
tree
2021-09-22
Andrew Reynolds
Add extensionality option for strings disequalities...
commit
|
commitdiff
|
tree
2021-09-22
Andrew Reynolds
Minimal fixing version for tuple update parsing (#7228)
commit
|
commitdiff
|
tree
2021-09-20
Andrew Reynolds
Add the LFSC proof post-processor (#7134)
commit
|
commitdiff
|
tree
next