projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Fast exit for string extended equality rewriter (#7312)
[cvc5.git]
/
src
/
theory
/
2021-10-07
Andrew Reynolds
Fast exit for string extended equality rewriter (#7312)
tree
|
commitdiff
2021-10-06
Andrew Reynolds
Eliminate more hard coded uses of user context (#7309)
tree
|
commitdiff
2021-10-05
Gereon Kremer
First round of refactoring on NlModel (#7255)
tree
|
commitdiff
2021-10-04
Andrew Reynolds
Refactor internally generated bounded quantified formul...
tree
|
commitdiff
2021-10-04
Andrew Reynolds
Move isFiniteType from theory engine to Env (#7287)
tree
|
commitdiff
2021-10-04
Andrew Reynolds
Eliminating static calls to rewriter in quantifiers...
tree
|
commitdiff
2021-10-04
Andrew Reynolds
Eliminating static calls to rewriter from strings ...
tree
|
commitdiff
2021-10-01
Andrew Reynolds
Update theory preprocessor to use Env (#7288)
tree
|
commitdiff
2021-10-01
Andrew Reynolds
Make preregistration safe for uninterpreted constants...
tree
|
commitdiff
2021-10-01
Andrew Reynolds
Use the proper evaluator for optimized SyGuS datatype...
tree
|
commitdiff
2021-10-01
Aina Niemetz
Rename SmtEngine to SolverEngine. (#7282)
tree
|
commitdiff
2021-09-30
Aina Niemetz
Rename files smt_engine.(cpp|h) to solver_engine.(cpp...
tree
|
commitdiff
2021-09-30
Mathias Preiner
bv: Refactor ppRewrite and move to TheoryBV. (#7271)
tree
|
commitdiff
2021-09-30
Andrew Reynolds
Make theory engine modules use Env (#7277)
tree
|
commitdiff
2021-09-30
Andrew Reynolds
Simplify the syntax and representation of the separatio...
tree
|
commitdiff
2021-09-30
Gereon Kremer
Remove usage of static options in arithmetic theory...
tree
|
commitdiff
2021-09-29
Abdalrhman Mohamed
Remove support for extended `(check-sat <term>)` comman...
tree
|
commitdiff
2021-09-29
Andrew Reynolds
Properly restrict PBE symmetry breaking for abduction...
tree
|
commitdiff
2021-09-29
Andrew Reynolds
Add the strings array solver (#7232)
tree
|
commitdiff
2021-09-24
Andrew Reynolds
Eliminate calls to Rewriter::rewrite from strings entai...
tree
|
commitdiff
2021-09-23
Andrew Reynolds
Generalize string enumerator for fixed length sequences...
tree
|
commitdiff
2021-09-23
Gereon Kremer
Eliminate Output macro in favor of simple Env functions...
tree
|
commitdiff
2021-09-23
Lachnitt
[proofs] Alethe: Translate THEORY_REWRITE (#7236)
tree
|
commitdiff
2021-09-23
Gereon Kremer
Refactor check interface of nonlinear extension (#7235)
tree
|
commitdiff
2021-09-23
Andrew Reynolds
More uses of EnvObj (#7230)
tree
|
commitdiff
2021-09-23
Abdalrhman Mohamed
Use `|` to print quoted strings in `set-info` command...
tree
|
commitdiff
2021-09-23
Andrew Reynolds
Implement alpha equivalence proofs (#7066)
tree
|
commitdiff
2021-09-22
Andrew Reynolds
Make cegqi subsolvers EnvObj (#7205)
tree
|
commitdiff
2021-09-22
Andrew Reynolds
Towards standard usage of evaluator (#7189)
tree
|
commitdiff
2021-09-22
Andrew Reynolds
Add extensionality option for strings disequalities...
tree
|
commitdiff
2021-09-22
Aina Niemetz
arrays: Use EnvObj::rewrite and EnvObj::options. (...
tree
|
commitdiff
2021-09-22
Aina Niemetz
arrays: Move type enumerator implementation to .cpp...
tree
|
commitdiff
2021-09-22
Gereon Kremer
Eliminate arithmetic proof macros (#7226)
tree
|
commitdiff
2021-09-21
Andres Noetzli
Fix handling of conversions between FP and reals (...
tree
|
commitdiff
2021-09-20
Aina Niemetz
TheoryModel: Use EnvObj::rewrite instead of Rewriter...
tree
|
commitdiff
2021-09-17
Andres Noetzli
Use a single `NodeManager` per thread (#7204)
tree
|
commitdiff
2021-09-17
Gereon Kremer
Replace write access to options by a local variable...
tree
|
commitdiff
2021-09-17
Gereon Kremer
Minor cleanup related to EnvObj (#7206)
tree
|
commitdiff
2021-09-16
Andrew Reynolds
Fix relevant domain for parametric operators (#7198)
tree
|
commitdiff
2021-09-15
Andrew Reynolds
Minor changes to E-matching utilities (#7062)
tree
|
commitdiff
2021-09-15
Andrew Reynolds
Eliminate global access to options:: from quantifiers...
tree
|
commitdiff
2021-09-14
Mathias Preiner
bv: Unify bit-blasting code for udiv and urem. (#7188)
tree
|
commitdiff
2021-09-14
Mathias Preiner
proofs: Properly track pre- and post-rewrites in bbAtom...
tree
|
commitdiff
2021-09-13
Andres Noetzli
Remove context getters from `TheoryState` (#7174)
tree
|
commitdiff
2021-09-13
Andrew Reynolds
Connect difficulty manager to TheoryEngine (#7161)
tree
|
commitdiff
2021-09-13
Aina Niemetz
FP: Rename FpConverter to FpWordBlaster. (#7170)
tree
|
commitdiff
2021-09-11
Gereon Kremer
Use StatisticsRegistry from Env (#7166)
tree
|
commitdiff
2021-09-11
Mathias Preiner
bv: Move IsPowerOfTwo rule to preprocessing pass and...
tree
|
commitdiff
2021-09-10
Aina Niemetz
FP: Enable caching in the theory inference manager...
tree
|
commitdiff
2021-09-10
Mathias Preiner
bv: Use EnvObj::rewrite() and EnvObj::options() in...
tree
|
commitdiff
2021-09-10
Aina Niemetz
FP: Use EnvObj::rewrite() and options() in theory_fp...
tree
|
commitdiff
2021-09-10
Aina Niemetz
FP: Do not send trivial lemmas. (#7167)
tree
|
commitdiff
2021-09-10
Andres Noetzli
Use C++17 attributes (#7154)
tree
|
commitdiff
2021-09-10
Mathias Preiner
bv: Use EnvObj::rewrite() and EnvObj::options() in...
tree
|
commitdiff
2021-09-09
Andres Noetzli
Remove `TheoryState::getEnv()` (#7163)
tree
|
commitdiff
2021-09-09
Andrew Reynolds
Add difficulty manager (#7151)
tree
|
commitdiff
2021-09-09
Andrew Reynolds
Disable shared selectors for quantified logics without...
tree
|
commitdiff
2021-09-09
Andres Noetzli
Remove `TheoryState::options()` (#7148)
tree
|
commitdiff
2021-09-09
Andrew Reynolds
Remove deprecated SyGuS method evaluateWithUnfolding...
tree
|
commitdiff
2021-09-08
Andrew Reynolds
Improve pre-skolemization, move quantifiers preprocess...
tree
|
commitdiff
2021-09-08
Andrew Reynolds
Towards standard usage of ExtendedRewriter (#7145)
tree
|
commitdiff
2021-09-08
Andrew Reynolds
Add option for using bound inference for relevant asser...
tree
|
commitdiff
2021-09-08
Andrew Reynolds
Use rewriteViaMethod instead of accessing builtin proof...
tree
|
commitdiff
2021-09-07
Andres Noetzli
Use `EnvObj` methods instead of `Theory` methods (...
tree
|
commitdiff
2021-09-07
Aina Niemetz
sygus: Eliminate calls to Rewriter::rewrite. (#7142)
tree
|
commitdiff
2021-09-03
Aina Niemetz
EnvObj: Add options(), context(), userContext(). (...
tree
|
commitdiff
2021-09-03
MikolasJanota
Avoiding duplicate search in maps (#7055)
tree
|
commitdiff
2021-09-03
Aina Niemetz
sygus: Make more classes derive from EnvObj. (#7140)
tree
|
commitdiff
2021-09-03
Andrew Reynolds
Standardize Rewriter::rewriteViaMethod call (#7119)
tree
|
commitdiff
2021-09-03
Andrew Reynolds
Make quantifier module classes derive from EnvObj ...
tree
|
commitdiff
2021-09-03
Aina Niemetz
sygus: Make CeSingleInv derive from EnvObj. (#7136)
tree
|
commitdiff
2021-09-03
Aina Niemetz
theory: Have more classes in theory with reference...
tree
|
commitdiff
2021-09-03
Aina Niemetz
theory: Have Theory and TheoryArith* derive from EnvObj...
tree
|
commitdiff
2021-09-02
Andrew Reynolds
Remove more instances of ufHo (#7087)
tree
|
commitdiff
2021-09-02
Andres Noetzli
Remove unused `Backtracker` (#7115)
tree
|
commitdiff
2021-09-02
Andres Noetzli
[Unit Tests] Fix bags rewrite test (#7114)
tree
|
commitdiff
2021-09-02
Aina Niemetz
rewriter: Make rewriteEqualityExt non-static. (#7110)
tree
|
commitdiff
2021-09-01
Aina Niemetz
Clean up TheoryEngine header according to code style...
tree
|
commitdiff
2021-09-01
Aina Niemetz
rewriter: Make registerTheoryRewriter non-static. ...
tree
|
commitdiff
2021-09-01
Aina Niemetz
rewriter: Make clearCaches non-static. (#7100)
tree
|
commitdiff
2021-09-01
Andrew Reynolds
Lazy proof reconstruction for strings theory solver...
tree
|
commitdiff
2021-08-31
Aina Niemetz
bv: Remove dump=bv-rewrites. (#7099)
tree
|
commitdiff
2021-08-31
yoni206
bv-to-int-module: implementations and stubs for transla...
tree
|
commitdiff
2021-08-31
Andrew Reynolds
Fix normal forms context-dependent simplification for...
tree
|
commitdiff
2021-08-30
mudathirmahgoub
Add kind BAG_MAP and its type rule to bags (#6503)
tree
|
commitdiff
2021-08-30
Andrew Reynolds
Fix proof equality engine for "no-explain" premises...
tree
|
commitdiff
2021-08-30
Andrew Reynolds
Fix quantifiers dynamic split module for parametric...
tree
|
commitdiff
2021-08-27
Andrew Reynolds
Expand definitions in sygus operators at the SMT level...
tree
|
commitdiff
2021-08-27
Andrew Reynolds
Add missing methods to Solver API for models (#7052)
tree
|
commitdiff
2021-08-26
Andrew Reynolds
Eliminate currentSmtEngine for subsolver calls (#7068)
tree
|
commitdiff
2021-08-26
Andrew Reynolds
Make datatype selector expansion to its own accessible...
tree
|
commitdiff
2021-08-26
Gereon Kremer
Improve integration of nonlinear arithmetic into the...
tree
|
commitdiff
2021-08-26
Gereon Kremer
Consolidate language types (#7065)
tree
|
commitdiff
2021-08-25
Gereon Kremer
Add missing include (#7067)
tree
|
commitdiff
2021-08-25
Andrew Reynolds
Eliminate calls to currentSmtEngine (#7060)
tree
|
commitdiff
2021-08-24
Andrew Reynolds
Split higher-order term database (#7045)
tree
|
commitdiff
2021-08-24
Andrew Reynolds
Refactor enumerator management in synth conjecture...
tree
|
commitdiff
2021-08-24
yoni206
bv-to-int: more implementations (#7051)
tree
|
commitdiff
2021-08-24
Andrew Reynolds
Uniform treatment of trusted theory inferences in proof...
tree
|
commitdiff
2021-08-23
Andrew Reynolds
Fix non-deterministism in quantified datatypes expansio...
tree
|
commitdiff
next