projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Eliminating static calls to rewriter from strings (#7302)
[cvc5.git]
/
src
/
theory
/
quantifiers
/
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-29
Andrew Reynolds
Properly restrict PBE symmetry breaking for abduction...
tree
|
commitdiff
2021-09-24
Andrew Reynolds
Eliminate calls to Rewriter::rewrite from strings entai...
tree
|
commitdiff
2021-09-23
Gereon Kremer
Eliminate Output macro in favor of simple Env functions...
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-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-13
Andres Noetzli
Remove context getters from `TheoryState` (#7174)
tree
|
commitdiff
2021-09-10
Andres Noetzli
Use C++17 attributes (#7154)
tree
|
commitdiff
2021-09-09
Andres Noetzli
Remove `TheoryState::getEnv()` (#7163)
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-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
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-02
Andrew Reynolds
Remove more instances of ufHo (#7087)
tree
|
commitdiff
2021-09-02
Aina Niemetz
rewriter: Make rewriteEqualityExt non-static. (#7110)
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-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
Consolidate language types (#7065)
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-23
Andrew Reynolds
Fix non-deterministism in quantified datatypes expansio...
tree
|
commitdiff
2021-08-23
Andrew Reynolds
Generalize inequality elimination in quantifiers rewrit...
tree
|
commitdiff
2021-08-23
Andrew Reynolds
Fix single invocation partition for higher-order (...
tree
|
commitdiff
2021-08-22
Andrew Reynolds
Prenex quantified formulas with user annotations by...
tree
|
commitdiff
2021-08-20
Andrew Reynolds
Simplify how user-provided quantifier attributes are...
tree
|
commitdiff
2021-08-20
Andrew Reynolds
More refactoring of set defaults (#7043)
tree
|
commitdiff
2021-08-18
Andres Noetzli
Minor fixes of policy for eliminating quantifiers ...
tree
|
commitdiff
2021-08-17
Andrew Reynolds
Refactoring theory-specific variable elimination in...
tree
|
commitdiff
2021-08-17
Andrew Reynolds
Fix policy for eliminating quantified formulas (#7017)
tree
|
commitdiff
2021-08-17
Andrew Reynolds
Improve conversion to skolems in expression miner ...
tree
|
commitdiff
2021-08-17
Gereon Kremer
Push Env class into TheoryState (#7012)
tree
|
commitdiff
2021-08-16
Gereon Kremer
Make Theory class use Env (#7011)
tree
|
commitdiff
2021-08-04
Andrew Reynolds
Add inference ids for remainder of sygus solver (#6977)
tree
|
commitdiff
2021-08-04
Mathias Preiner
syqi: Add debug information for dumping instantiations...
tree
|
commitdiff
2021-08-04
Andrew Reynolds
Add optional debug information for dumping instantiatio...
tree
|
commitdiff
2021-08-04
Andrew Reynolds
Add missing inference identifiers (#6962)
tree
|
commitdiff
2021-07-28
Andrew Reynolds
Make extended rewriter methods const (#6948)
tree
|
commitdiff
2021-07-27
Andrew Reynolds
Track instantiation reasons in proofs (#6935)
tree
|
commitdiff
2021-07-27
Andrew Reynolds
Move enum value generator to own file (#6941)
tree
|
commitdiff
2021-07-27
Andrew Reynolds
Minor fix for term database + central equality engine...
tree
|
commitdiff
2021-07-27
Andrew Reynolds
Make all dependencies in the fast enumerator optional...
tree
|
commitdiff
2021-07-27
Andrew Reynolds
Add sygus enumerator callback (#6923)
tree
|
commitdiff
2021-07-16
Andrew Reynolds
Do not exhaustive instantiation when FMF is disabled...
tree
|
commitdiff
2021-07-15
Andrew Reynolds
Fix context for proofs of instantiations (#6890)
tree
|
commitdiff
2021-07-15
Andrew Reynolds
Distinguish quantifiers preprocess as its own proof...
tree
|
commitdiff
2021-07-15
Andrew Reynolds
Move master equality engine notification to own file...
tree
|
commitdiff
2021-07-14
Andrew Reynolds
Move synthesis verification check to own file (#6882)
tree
|
commitdiff
2021-07-07
Andrew Reynolds
Standard output for trigger selection (#6841)
tree
|
commitdiff
2021-07-03
Andres Noetzli
Fix performance of string regression (#6832)
tree
|
commitdiff
2021-07-03
Mathias Preiner
Add output tags -o, --output. (#6826)
tree
|
commitdiff
2021-07-01
Andrew Reynolds
Add recursive function definitions to subsolver in...
tree
|
commitdiff
2021-07-01
Andrew Reynolds
Add option to limit the number of instantiation rounds...
tree
|
commitdiff
2021-06-30
Andrew Reynolds
Do not apply fmfBound to standard quantifiers when...
tree
|
commitdiff
2021-06-28
Andrew Reynolds
Rename internal string kinds to match API (#6797)
tree
|
commitdiff
2021-06-22
Andrew Reynolds
Fix type enumeration for non first-class sorts in FMF...
tree
|
commitdiff
2021-06-15
Gereon Kremer
Remove public option wrappers (#6716)
tree
|
commitdiff
2021-06-08
Andrew Reynolds
Fix for 2 dimensional dependent bounded quantifiers...
tree
|
commitdiff
2021-06-07
Gereon Kremer
Remove `Options::wasSetByUser()` (#6682)
tree
|
commitdiff
2021-06-02
Gereon Kremer
Move public wrapper functions out of options class...
tree
|
commitdiff
2021-05-27
Andrew Reynolds
Fix CEGQI for datatypes with Boolean subfields (#6630)
tree
|
commitdiff
2021-05-27
Aina Niemetz
FP: Rename FLOATINGPOINT_PLUS to FLOATINGPOINT_ADD...
tree
|
commitdiff
2021-05-26
Andres Noetzli
More precise includes of `Node` constants (#6617)
tree
|
commitdiff
2021-05-24
Andrew Reynolds
Move proof utilities to src/proof/ (#6611)
tree
|
commitdiff
2021-05-24
Andrew Reynolds
Fix instance of no rewrite in extended rewriter (#6610)
tree
|
commitdiff
2021-05-21
Andrew Reynolds
Fix and refactor relevant domain (#6528)
tree
|
commitdiff
2021-05-21
Andrew Reynolds
Update to sygus standard output for check-synth respons...
tree
|
commitdiff
2021-05-21
Aina Niemetz
BV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589)
tree
|
commitdiff
2021-05-20
Haniel Barbosa
Remove old unsat cores (#6581)
tree
|
commitdiff
2021-05-18
Abdalrhman Mohamed
Loop over terms to reconstruct instead of obligations...
tree
|
commitdiff
2021-05-13
Mathias Preiner
Add std::hash overloads for Node, TNode and TypeNode...
tree
|
commitdiff
2021-05-07
Andrew Reynolds
Simplifications to expand definitions (#6487)
tree
|
commitdiff
2021-05-06
Andrew Reynolds
Discard duplicate terms in patterns (#6501)
tree
|
commitdiff
2021-05-05
Andrew Reynolds
Do not have quantifiers model inherit from theory model...
tree
|
commitdiff
2021-04-29
Gereon Kremer
Avoid exponential explosion of small constant in CEGQI...
tree
|
commitdiff
2021-04-28
Gereon Kremer
Remove exception headers from options.h (#6456)
tree
|
commitdiff
2021-04-27
Andrew Reynolds
Fix refutational soundness bug in quantifier prenexing...
tree
|
commitdiff
2021-04-26
Gereon Kremer
First part of options refactoring (#6428)
tree
|
commitdiff
2021-04-25
Andrew Reynolds
Use fast enumeration by default for Boolean predicate...
tree
|
commitdiff
2021-04-23
Andrew Reynolds
Enable strings exp by default for strings specific...
tree
|
commitdiff
2021-04-21
Mathias Preiner
Goodbye CVC4, hello cvc5! (#6371)
tree
|
commitdiff
2021-04-20
Aina Niemetz
Quantifiers: Move implementation of type rules to cpp...
tree
|
commitdiff
2021-04-19
Andrew Reynolds
Fully incorporate quantifiers macros into ppAssert...
tree
|
commitdiff
2021-04-15
Aina Niemetz
Rename occurrences of CVC4 to CVC5. (#6351)
tree
|
commitdiff
2021-04-14
Gereon Kremer
Refactor / reimplement statistics (#6162)
tree
|
commitdiff
next