projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Add support for re.all (#2980)
[cvc5.git]
/
src
/
smt
/
2019-04-30
Andrew Reynolds
Eliminate APPLY kind (#2976)
tree
|
commitdiff
2019-04-24
Mathias Preiner
Do not use __ prefix for header guards. (#2974)
tree
|
commitdiff
2019-04-17
Andrew Reynolds
More use of isClosure (#2959)
tree
|
commitdiff
2019-04-11
Andrew Reynolds
Eliminate Boolean ITE within terms, fixes 2947 (#2949)
tree
|
commitdiff
2019-03-26
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2019-03-22
makaimann
Use empty vector instead of false in query with null...
tree
|
commitdiff
2019-03-20
Andrew Reynolds
Sygus abduction feature (#2744)
tree
|
commitdiff
2019-03-16
Andres Noetzli
Limit --solve-int-as-bv=X to QF_NIA/QF_LIA/QF_IDL ...
tree
|
commitdiff
2019-03-14
makaimann
check for null assumption in query and replace with...
tree
|
commitdiff
2019-03-13
Andres Noetzli
Add statistics for proof gen./checking time, size ...
tree
|
commitdiff
2019-02-27
Andres Noetzli
Use string stream for proofs instead of tmp files ...
tree
|
commitdiff
2019-02-12
Andres Noetzli
Delete temporary proof files when aborting CVC4 (#2834)
tree
|
commitdiff
2019-01-18
Andres Noetzli
Fix ABC build (#2808)
tree
|
commitdiff
2019-01-15
Andres Noetzli
Strings: Add option to change loop process mode (#2794)
tree
|
commitdiff
2019-01-11
Aina Niemetz
New C++ API: Add unit tests for setInfo, setLogic,...
tree
|
commitdiff
2018-12-11
Andrew Reynolds
Remove alternate versions of mbqi (#2742)
tree
|
commitdiff
2018-12-10
makaimann
BoolToBV modes (off, ite, all) (#2530)
tree
|
commitdiff
2018-12-06
Andres Noetzli
Fix use-after-free due to destruction order (#2739)
tree
|
commitdiff
2018-11-29
Andrew Reynolds
Combine sygus stream with PBE (#2726)
tree
|
commitdiff
2018-11-27
Andrew Reynolds
Lazy model construction in TheoryEngine (#2633)
tree
|
commitdiff
2018-11-21
Andrew Reynolds
Quickly recognize when PBE conjectures are infeasible...
tree
|
commitdiff
2018-11-15
Andrew Reynolds
Expand definitions prior to model core computation...
tree
|
commitdiff
2018-10-31
Andres Noetzli
Record assumption info in AssertionPipeline (#2678)
tree
|
commitdiff
2018-10-22
Andres Noetzli
Recover from wrong use of get-info :reason-unknown...
tree
|
commitdiff
2018-10-20
Andrew Reynolds
Sygus streaming non-implied predicates (#2660)
tree
|
commitdiff
2018-10-19
Andres Noetzli
Add OptionException handling during initialization...
tree
|
commitdiff
2018-10-19
Andrew Reynolds
Non-implied mode for model cores (#2653)
tree
|
commitdiff
2018-10-18
Haniel Barbosa
Introducing internal commands for SyGuS commands (...
tree
|
commitdiff
2018-10-18
Andrew Reynolds
Sygus query generator (#2465)
tree
|
commitdiff
2018-10-15
Andrew Reynolds
Delay initialization of theory engine (#2621)
tree
|
commitdiff
2018-10-13
Andres Noetzli
Reset input language for ExprMiner subsolver (#2624)
tree
|
commitdiff
2018-10-11
Haniel Barbosa
Fix default setting of CegisUnif options (#2605)
tree
|
commitdiff
2018-10-11
Andrew Reynolds
Synthesize rewrite rules from inputs (#2608)
tree
|
commitdiff
2018-10-09
Aina Niemetz
Fix compiler warnings. (#2601)
tree
|
commitdiff
2018-10-05
Andrew Reynolds
Update default options for sygus (#2586)
tree
|
commitdiff
2018-10-01
Andres Noetzli
Fix dumping pre/post preprocessing passes (#2469)
tree
|
commitdiff
2018-10-01
Andres Noetzli
Refactor preprocessing pass registration (#2468)
tree
|
commitdiff
2018-09-22
Mathias Preiner
cmake: Remove unused CMakeLists.txt
tree
|
commitdiff
2018-09-22
Aina Niemetz
cmake: Added initial build infrastructure.
tree
|
commitdiff
2018-09-18
Andrew Reynolds
Move and rename sygus solver classes (#2488)
tree
|
commitdiff
2018-09-18
Haniel Barbosa
fix assertion error (#2487)
tree
|
commitdiff
2018-09-17
Andres Noetzli
Remove broken dumping support from portfolio build...
tree
|
commitdiff
2018-09-17
Andres Noetzli
Remove unnecessary tracing from preprocessing (#2472)
tree
|
commitdiff
2018-09-15
Andres Noetzli
Refactor how assertions are added to decision engine...
tree
|
commitdiff
2018-09-11
Andrew Reynolds
Support model cores via option --produce-model-cores...
tree
|
commitdiff
2018-09-11
Aina Niemetz
Refactor non-clausal simplify preprocessing pass. ...
tree
|
commitdiff
2018-09-05
Andrew Reynolds
Finer-grained inference of substitutions in incremental...
tree
|
commitdiff
2018-09-04
Aina Niemetz
Transfer ownership of learned literals from SMT engine...
tree
|
commitdiff
2018-09-04
Aina Niemetz
Fix merge mishap of #2359.
tree
|
commitdiff
2018-08-30
Mathias Preiner
Refactor theory preprocess into preprocessing pass...
tree
|
commitdiff
2018-08-29
Mathias Preiner
Refactor MipLibTrick preprocessing pass. (#2359)
tree
|
commitdiff
2018-08-28
Aina Niemetz
Move flag needsFinish from SMT engine to circuit propag...
tree
|
commitdiff
2018-08-26
Andres Noetzli
Refactor unconstrained simplification pass (#2374)
tree
|
commitdiff
2018-08-25
yoni206
Refactor quantifier macros preprocessing pass (#1840)
tree
|
commitdiff
2018-08-25
Haniel Barbosa
Refactor nlExtPurify preprocessing pass (#1963)
tree
|
commitdiff
2018-08-24
Andrew Reynolds
Remove spurious disabling of cbqi-all (#2368)
tree
|
commitdiff
2018-08-24
Andrew Reynolds
Do not print internally generated datatypes in externa...
tree
|
commitdiff
2018-08-23
Haniel Barbosa
Makes the filename be set in the SMT engine by default...
tree
|
commitdiff
2018-08-23
Aina Niemetz
Refactor ITE simplification preprocessing pass. (#2360)
tree
|
commitdiff
2018-08-23
Andres Noetzli
Use "filename" instead of "name" in SmtEngine::setInfo...
tree
|
commitdiff
2018-08-23
yoni206
global-negate preprocessing pass (#2317)
tree
|
commitdiff
2018-08-21
Tim King
Removing unused bool members in command.cpp. Also initi...
tree
|
commitdiff
2018-08-21
Mathias Preiner
Move d_realAssertionsEnd from SmtEnginePrivate to Asser...
tree
|
commitdiff
2018-08-21
Andrew Reynolds
Use cbqi-full for sygus (#2346)
tree
|
commitdiff
2018-08-20
Andrew Reynolds
Make sygus inference a preprocessing pass (#2334)
tree
|
commitdiff
2018-08-17
Andrew Reynolds
Eliminate partial operators in sygus grammar normaliza...
tree
|
commitdiff
2018-08-17
Mathias Preiner
Refactor eager atoms preprocessing pass. (#2318)
tree
|
commitdiff
2018-08-17
Haniel Barbosa
cleaning unnecessary timers/dumps (#2327)
tree
|
commitdiff
2018-08-17
Caleb Donovick
Make quantifiers-preprocess preprocessing pass (#2322)
tree
|
commitdiff
2018-08-17
Andres Noetzli
Refactor IteRemoval preprocessing pass (#1793)
tree
|
commitdiff
2018-08-16
Andres Noetzli
Move node algorithms to separate file (#2311)
tree
|
commitdiff
2018-08-16
Haniel Barbosa
Refactor extended rewriter preprocessing pass (#2324)
tree
|
commitdiff
2018-08-16
Haniel Barbosa
Refactor apply2const (#2316)
tree
|
commitdiff
2018-08-15
Andres Noetzli
Remove unused tuple classes (#2313)
tree
|
commitdiff
2018-08-15
Andrew Reynolds
Make sort inference a preprocessing pass (#2309)
tree
|
commitdiff
2018-08-15
Andres Noetzli
Fix dumping of get-unsat-assumptions (#2302)
tree
|
commitdiff
2018-08-14
Andres Noetzli
Fix get-unsat-assumptions output (#2301)
tree
|
commitdiff
2018-08-08
Andrew Reynolds
Do beta-reduction in expandDefinitions (#2286)
tree
|
commitdiff
2018-08-08
Andres Noetzli
Require Swig 3 (#2283)
tree
|
commitdiff
2018-08-08
Andres Noetzli
Delete functions instead of using CVC4_UNDEFINED (...
tree
|
commitdiff
2018-08-07
Andrew Reynolds
Move sygus quantifier elimination step for non-ground...
tree
|
commitdiff
2018-08-06
Andrew Reynolds
Fixes for sygus inference (#2238)
tree
|
commitdiff
2018-08-02
Andres Noetzli
Remove outdated references to TLS (#2245)
tree
|
commitdiff
2018-08-02
Andrew Reynolds
Fix issues with printing parametric datatypes in smt2...
tree
|
commitdiff
2018-08-01
ayveejay
Improvements and tests for the API around separation...
tree
|
commitdiff
2018-07-31
Mathias Preiner
Fix option handler for lazy/bv-sat-solver combinations...
tree
|
commitdiff
2018-07-30
Mathias Preiner
Add support for incremental eager bit-blasting. (#1838)
tree
|
commitdiff
2018-07-27
Andrew Reynolds
Make check-synth robust for assertions that are not...
tree
|
commitdiff
2018-07-26
yoni206
Disabling bvLazyRewriteExtf in the right place (#2214)
tree
|
commitdiff
2018-07-25
ayveejay
Performing clang-format on the original change-set...
tree
|
commitdiff
2018-07-24
ayveejay
Adding API access methods to get heap/nil expressions...
tree
|
commitdiff
2018-07-23
Andrew Reynolds
Generalize symmetry detection for 1 symmetry variable...
tree
|
commitdiff
2018-07-17
yoni206
Refactor sep-pre-skolem-emp preprocessing pass
tree
|
commitdiff
2018-07-17
Andrew Reynolds
Do extended rewrite on results of quantifier eliminatio...
tree
|
commitdiff
2018-07-11
Caleb Donovick
Move rewrite to pass (#2128)
tree
|
commitdiff
2018-07-03
Andrew Reynolds
sygusComp2018: update sygus-related options setting...
tree
|
commitdiff
2018-07-03
Andrew Reynolds
Remove miscellaneous dead and unused code from quantifi...
tree
|
commitdiff
2018-07-02
Aina Niemetz
Refactor ApplySubsts preprocessing pass. (#2120)
tree
|
commitdiff
2018-07-02
Caleb Donovick
Add missing include (#2127)
tree
|
commitdiff
2018-06-27
Andrew Reynolds
Synthesize candidate-rewrites from standard inputs...
tree
|
commitdiff
next