projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Split abduction solver from SmtEngine (#4733)
[cvc5.git]
/
src
/
smt
/
smt_engine.h
2020-07-15
Andrew Reynolds
Split abduction solver from SmtEngine (#4733)
blob
|
commitdiff
|
raw
2020-07-07
Andrew Reynolds
Transfer ownership of internal Options from NodeManager...
blob
|
commitdiff
|
raw
|
diff to current
2020-06-30
Ying Sheng
Interpolation step 1 (#4638)
blob
|
commitdiff
|
raw
|
diff to current
2020-06-25
Andrew Reynolds
Remove sygus1 parser (#4651)
blob
|
commitdiff
|
raw
|
diff to current
2020-06-19
Andres Noetzli
Add logic check for define-fun(s)-rec (#4577)
blob
|
commitdiff
|
raw
|
diff to current
2020-06-16
Aina Niemetz
Update copyright headers.
blob
|
commitdiff
|
raw
|
diff to current
2020-06-06
Andres Noetzli
Keep definitions when global-declarations enabled ...
blob
|
commitdiff
|
raw
|
diff to current
2020-06-04
Aina Niemetz
New C++ Api: Second and last batch of API guards. ...
blob
|
commitdiff
|
raw
|
diff to current
2020-04-09
Andrew Reynolds
Split ProcessAssertions module from SmtEngine (#4210)
blob
|
commitdiff
|
raw
|
diff to current
2020-04-03
Andres Noetzli
Update theory rewriter ownership, add stats to strings...
blob
|
commitdiff
|
raw
|
diff to current
2020-04-01
Aina Niemetz
Rename checkValid/query to checkEntailed. (#4191)
blob
|
commitdiff
|
raw
|
diff to current
2020-03-31
Andrew Reynolds
Remove replay and use-theory options and idl (#4186)
blob
|
commitdiff
|
raw
|
diff to current
2020-03-27
Andrew Reynolds
Move set defaults function to its own file (#4154)
blob
|
commitdiff
|
raw
|
diff to current
2020-03-17
Aina Niemetz
SmtEngine: Convert members owned by SmtEngine to unique...
blob
|
commitdiff
|
raw
|
diff to current
2020-03-10
Aina Niemetz
Fix issue with reset-assertions. (#3988)
blob
|
commitdiff
|
raw
|
diff to current
2020-03-05
Aina Niemetz
Move ownership of DecisionEngine into PropEngine. ...
blob
|
commitdiff
|
raw
|
diff to current
2020-03-05
Aina Niemetz
Revert "Move ownership of DecisionEngine into PropEngin...
blob
|
commitdiff
|
raw
|
diff to current
2020-03-05
Andrew Reynolds
Move ownership of DecisionEngine into PropEngine. ...
blob
|
commitdiff
|
raw
|
diff to current
2020-02-26
Andres Noetzli
Remove portfolio leftovers (#3821)
blob
|
commitdiff
|
raw
|
diff to current
2019-11-13
Andrew Reynolds
Distinguish unknown status for model printing (#3454)
blob
|
commitdiff
|
raw
|
diff to current
2019-11-04
Andrew Reynolds
Make getSynthSolution return a Bool (#3306)
blob
|
commitdiff
|
raw
|
diff to current
2019-09-04
Andrew Reynolds
Towards incremental SyGuS in SMT engine (#3195)
blob
|
commitdiff
|
raw
|
diff to current
2019-08-19
Aina Niemetz
New C++ API: Add checks for Solver::checkValid and...
blob
|
commitdiff
|
raw
|
diff to current
2019-08-14
Andrew Reynolds
Call separate SMT engine for single invocation sygus...
blob
|
commitdiff
|
raw
|
diff to current
2019-08-14
Aina Niemetz
SmtEngine: Reorganize class according to guidelines...
blob
|
commitdiff
|
raw
|
diff to current
2019-08-13
Andrew Reynolds
Track sygus variable to term relationship via attribut...
blob
|
commitdiff
|
raw
|
diff to current
2019-08-13
Andrew Reynolds
Implement check abduct feature (#3152)
blob
|
commitdiff
|
raw
|
diff to current
2019-08-07
Aina Niemetz
New C++ API: Add checks and tests for push/pop. (#3121)
blob
|
commitdiff
|
raw
|
diff to current
2019-08-02
Andrew Reynolds
Flip the polarity of the argument of get-abduct (#3153)
blob
|
commitdiff
|
raw
|
diff to current
2019-07-30
Andrew Reynolds
Track solver execution mode (#3132)
blob
|
commitdiff
|
raw
|
diff to current
2019-07-29
Andrew Reynolds
Model blocker feature (#3112)
blob
|
commitdiff
|
raw
|
diff to current
2019-07-29
Andrew Reynolds
Support get-abduct smt2 command (#3122)
blob
|
commitdiff
|
raw
|
diff to current
2019-06-04
Andres Noetzli
Add check that result matches benchmark status (#3028)
blob
|
commitdiff
|
raw
|
diff to current
2019-04-24
Mathias Preiner
Do not use __ prefix for header guards. (#2974)
blob
|
commitdiff
|
raw
|
diff to current
2019-03-26
Aina Niemetz
Update copyright headers.
blob
|
commitdiff
|
raw
|
diff to current
2019-03-20
Andrew Reynolds
Sygus abduction feature (#2744)
blob
|
commitdiff
|
raw
|
diff to current
2019-01-11
Aina Niemetz
New C++ API: Add unit tests for setInfo, setLogic,...
blob
|
commitdiff
|
raw
|
diff to current
2018-10-18
Haniel Barbosa
Introducing internal commands for SyGuS commands (...
blob
|
commitdiff
|
raw
|
diff to current
2018-08-23
Haniel Barbosa
Makes the filename be set in the SMT engine by default...
blob
|
commitdiff
|
raw
|
diff to current
2018-08-15
Andres Noetzli
Fix dumping of get-unsat-assumptions (#2302)
blob
|
commitdiff
|
raw
|
diff to current
2018-08-08
Andres Noetzli
Delete functions instead of using CVC4_UNDEFINED (...
blob
|
commitdiff
|
raw
|
diff to current
2018-08-01
ayveejay
Improvements and tests for the API around separation...
blob
|
commitdiff
|
raw
|
diff to current
2018-07-24
ayveejay
Adding API access methods to get heap/nil expressions...
blob
|
commitdiff
|
raw
|
diff to current
2018-05-22
Andrew Reynolds
Make sygus infer find function definitions (#1951)
blob
|
commitdiff
|
raw
|
diff to current
2018-03-13
Aina Niemetz
SmtEngine::getModel() is now public. (#1665)
blob
|
commitdiff
|
raw
|
diff to current
2018-03-09
Aina Niemetz
Add support for SMT-LIB v2.5 command get-unsat-assumpti...
blob
|
commitdiff
|
raw
|
diff to current
2018-03-05
Aina Niemetz
Add support for check-sat-assuming. (#1637)
blob
|
commitdiff
|
raw
|
diff to current
2018-03-02
Aina Niemetz
Fixed comments in smt_engine.h.
blob
|
commitdiff
|
raw
|
diff to current
2018-02-28
Aina Niemetz
SmtEngine::getAssignment now returns a vector of assign...
blob
|
commitdiff
|
raw
|
diff to current
2018-02-02
Haniel Barbosa
Option to check solutions produced by SyGuS solver...
blob
|
commitdiff
|
raw
|
diff to current
2018-01-25
Tim King
Commenting out throw specifiers on SmtEngine. These...
blob
|
commitdiff
|
raw
|
diff to current
2018-01-03
Andrew Reynolds
Global negate (#1466)
blob
|
commitdiff
|
raw
|
diff to current
2017-12-11
justinxu421
Add new infrastructure for preprocessing passes (#1053)
blob
|
commitdiff
|
raw
|
diff to current
2017-12-07
Andrew Reynolds
Add command for define-fun-rec and add to API (#1412)
blob
|
commitdiff
|
raw
|
diff to current
2017-11-15
Tim King
Adding garbage collection for Proof objects. (#1294)
blob
|
commitdiff
|
raw
|
diff to current
2017-11-07
Andrew Reynolds
Allow FORALL in quantifier elimination command (#1322)
blob
|
commitdiff
|
raw
|
diff to current
2017-10-11
Andrew Reynolds
Move unsat core names to smt engine (#1192)
blob
|
commitdiff
|
raw
|
diff to current
2017-09-14
Tim King
Simplifying the throw specifier of SmtEngine::checkSat...
blob
|
commitdiff
|
raw
|
diff to current
2017-07-21
Tim King
Merge branch 'master' into cleanup-regexp
blob
|
commitdiff
|
raw
|
diff to current
2017-07-20
Tim King
Removing the unused CDAttribute. This makes CDHashMap...
blob
|
commitdiff
|
raw
|
diff to current
2017-07-07
Mathias Preiner
Update copyright headers.
blob
|
commitdiff
|
raw
|
diff to current
2017-05-12
Andres Notzli
Make signal handlers safer
blob
|
commitdiff
|
raw
|
diff to current
2017-04-04
Clark Barrett
Merge pull request #141 from 4tXJ7f/remove_def
blob
|
commitdiff
|
raw
|
diff to current
2017-03-31
Andres Notzli
Remove decl. of getStatisticsRegistry(SmtEngine*)
blob
|
commitdiff
|
raw
|
diff to current
2017-03-30
Clark Barrett
Merge pull request #139 from 4tXJ7f/remove_throw
blob
|
commitdiff
|
raw
|
diff to current
2017-03-30
Andres Notzli
[Coverity] Remove throw qualifiers in src/smt
blob
|
commitdiff
|
raw
|
diff to current
2016-11-04
ajreynol
Fix a few more minor memory leaks.
blob
|
commitdiff
|
raw
|
diff to current
2016-10-28
ajreynol
Add get instantiations utilities to API.
blob
|
commitdiff
|
raw
|
diff to current
2016-04-20
PaulMeng
update from the master
blob
|
commitdiff
|
raw
|
diff to current
2016-04-09
Guy
Merge branch 'master' of https://github.com/CVC4/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2016-04-04
Tim King
Updating the copyright headers and scripts.
blob
|
commitdiff
|
raw
|
diff to current
2016-03-22
Tim King
Deleting the contents of d_modelGlobalsCommands before...
blob
|
commitdiff
|
raw
|
diff to current
2016-03-08
ajreynol
Extend synthesis solver to handle single invocation...
blob
|
commitdiff
|
raw
|
diff to current
2016-02-17
ajreynol
Refactor quantifiers attributes. Make quantifier elimin...
blob
|
commitdiff
|
raw
|
diff to current
2016-02-16
ajreynol
Public interface for quantifier elimination. Minor...
blob
|
commitdiff
|
raw
|
diff to current
2016-01-28
Tim King
Adding listeners to Options.
blob
|
commitdiff
|
raw
|
diff to current
2016-01-09
Tim King
Removing StatisticsRegistry's static functions current...
blob
|
commitdiff
|
raw
|
diff to current
2016-01-06
Tim King
Moving sexpr.{cpp,h,i} from expr/ back into util/.
blob
|
commitdiff
|
raw
|
diff to current
2016-01-06
Tim King
Add SmtGlobals Class
blob
|
commitdiff
|
raw
|
diff to current
2015-12-15
Tim King
Refactoring Options Handler & Library Cycle Breaking
blob
|
commitdiff
|
raw
|
diff to current
2015-10-26
Tim King
This commit fixes a bug related to a public header...
blob
|
commitdiff
|
raw
|
diff to current
2015-07-31
ajreynol
Make --fmf-fun and --macros-quant work in incremental...
blob
|
commitdiff
|
raw
|
diff to current
2015-07-31
ajreynol
Sygus support for inductive datatypes.
blob
|
commitdiff
|
raw
|
diff to current
2015-05-12
barrettcw
Merge pull request #74 from finnhaedicke/namespace_minisat
blob
|
commitdiff
|
raw
|
diff to current
2015-04-23
Clark Barrett
Merge branch 'master' into google
blob
|
commitdiff
|
raw
|
diff to current
2015-04-23
Liana Hadarean
Added option for --check-unsat-cores and various core...
blob
|
commitdiff
|
raw
|
diff to current
2015-02-06
Tianyi Liang
Merge branch 'master' of github.com:tiliang/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2015-01-26
ajreynol
Output solutions for synthesis conjectures with --dump...
blob
|
commitdiff
|
raw
|
diff to current
2014-11-27
Tianyi Liang
Merge branch 'master' of github.com:tiliang/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2014-11-17
Liana Hadarean
Resource-limiting work.
blob
|
commitdiff
|
raw
|
diff to current
2014-11-10
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-11-07
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-11-07
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-11-07
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-11-05
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-10-23
Morgan Deters
Parsing and infrastructure support for SMT-LIBv2.5...
blob
|
commitdiff
|
raw
|
diff to current
2014-10-17
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-10-16
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-10-14
Morgan Deters
Merge pull request #58 from mdeters/smt-attributes
blob
|
commitdiff
|
raw
|
diff to current
2014-10-14
Morgan Deters
Context-dependent expr attributes are now attached...
blob
|
commitdiff
|
raw
|
diff to current
next