Age | Commit message (Collapse) | Author | |
---|---|---|---|
2015-05-28 | added options for controlling resource step-count for various solving stages | Liana Hadarean | |
2015-05-11 | Allow sygus with no syntactic restrictions for LIA. Add regressions. | ajreynol | |
2015-05-11 | Support for arbitrary constants/variables in Sygus grammars. | ajreynol | |
2015-04-24 | More parser related bug fixes (define-funs-rec, declare-funs). Bug fix for ↵ | ajreynol | |
fmf mbqi=gen-ev for interpreted operators. | |||
2015-04-24 | Fix sygus parser for non-tokenized operators, reenable regression. Fix for ↵ | ajreynol | |
--fmf-fun. | |||
2015-04-23 | Added option for --check-unsat-cores and various core bug fixes (merge of ↵ | Liana Hadarean | |
Morgan's proof branch). | |||
2015-04-22 | Merge pull request #73 from kbansal/parser-dont-tokenize | Kshitij Bansal | |
Parser dont tokenize | |||
2015-04-16 | Handle (degenerate) case of synthesis conjectures for constants. Disable ↵ | ajreynol | |
delta lemmas. | |||
2015-04-16 | update comment | Kshitij Bansal | |
2015-04-15 | string parser builtinop changes | Kshitij Bansal | |
2015-04-15 | bv parserchanges cleanup | Kshitij Bansal | |
2015-04-15 | fp builtinop parser changes | Kshitij Bansal | |
2015-04-15 | fp reorder tokens to match other occurences | Kshitij Bansal | |
2015-04-15 | THEORY_INTS parser changes | Kshitij Bansal | |
2015-04-15 | THEORY_REAL_INTS parser changes | Kshitij Bansal | |
2015-04-15 | array theory builtinop | Kshitij Bansal | |
2015-04-15 | cleanup | Kshitij Bansal | |
2015-04-15 | dont tokenize bv operators (normal ones) | Kshitij Bansal | |
2015-04-08 | Make fun-def quantifiers carry the function app they define, make fun-def ↵ | ajreynol | |
utilities more robust. Fix bug in conjecture generation for non-parameterized operators. | |||
2015-03-23 | Parsing support for define-fun-rec/define-funs-rec. | ajreynol | |
2015-03-05 | Minor fixes. Extend cegqi-si to real arithmetic. | ajreynol | |
2015-02-13 | Handle recursive singleton case for codatatypes, add regression. Simplify ↵ | ajreynol | |
implementation of datatype utility: fixes well-foundedness check and mkGroundTerm for parametric datatypes. | |||
2015-02-06 | Handle missing cases for single inv solution reconstruction. Minor fixes. ↵ | ajreynol | |
Refactor. | |||
2015-01-26 | Output solutions for synthesis conjectures with --dump-synth. Minor ↵ | ajreynol | |
refactor of previous commit. | |||
2015-01-23 | Rework inst-closure. | ajreynol | |
2015-01-22 | Add option --lte-partial-inst. Remove inst-closure. | ajreynol | |
2015-01-21 | Initial work on sygusNormalForm. | ajreynol | |
2015-01-20 | Mark datatypes as sygus. Add option to normalize sygus terms in search. ↵ | ajreynol | |
Add sygus regressions. | |||
2015-01-20 | Handle miniscoping of conjunctions in synthesis properties. Refactor ↵ | ajreynol | |
construction of sygus datatypes. Expand define-fun in evaluators. | |||
2015-01-17 | Avoid name conflicts for multiple synth-fun. | ajreynol | |
2015-01-16 | Linearize multiplication by constants in sygus grammars. Handle unary minus ↵ | ajreynol | |
integer numerals. Refactor to smt2.cpp. | |||
2015-01-16 | Allow uninterpreted/defined functions in Sygus grammars. Fix bug regarding ↵ | ajreynol | |
declare-var vs synth-fun arguments. Handle ground properties in sythesis conjectures. | |||
2015-01-16 | Minor: Ensure indexed terms are in EE. Add support for bv constants in ↵ | ajreynol | |
sygus parser. | |||
2015-01-14 | sygus input language and benchmark | Morgan Deters | |
2015-01-13 | Remove private #include. | Morgan Deters | |
2015-01-13 | Fix typo. | Morgan Deters | |
2015-01-09 | blocked unprintable characters in string literals; | Tianyi Liang | |
disabled string literal test case for smtlib v2.5 | |||
2014-12-12 | Add cvc parsing support for cardinality constraints. Bug fix for ↵ | ajreynol | |
enumerating elements to meet cardinality lower bounds. | |||
2014-12-03 | Floating point infrastructure. | Martin Brain | |
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu> | |||
2014-11-25 | Fix bug in --term-db-mode=relevant with variable triggers. Support ↵ | ajreynol | |
inst-closure predicate and mode --term-db-inst-closure. Minor changes to theory_quantifiers. | |||
2014-11-17 | Resource-limiting work. | Liana Hadarean | |
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu> | |||
2014-11-12 | Fix tokenization of "reset" in SMT-LIB v2.0. It's a reserved word only in 2.5. | Morgan Deters | |
2014-10-28 | Preprocessing step for finding finite runs of well-defined function ↵ | ajreynol | |
definitions using FMF. | |||
2014-10-28 | Initial infrastructure for function definition quantifiers, internal parsing ↵ | ajreynol | |
format for Smt2. | |||
2014-10-24 | Minor parser performance fix. | Morgan Deters | |
2014-10-23 | Parsing and infrastructure support for SMT-LIBv2.5 input and output languages. | Morgan Deters | |
* support for new commands meta-info, declare-const, echo, get-model, reset, and reset-assertions * support for set-option :global-declarations * support for set-option :produce-assertions * support for set-option :reproducible-resource-limit * support for get-info :assertion-stack-levels * support for set-info :smt-lib-version 2.5 * ascribe types for abstract values (the new 2.5 standard clarifies that this is required) * SMT-LIB v2.5 string literals (we still support 2.0 string literals when in 2.0 mode) What's still to do: * check-sat-assumptions/get-unsat-assumptions (still being hotly debated). Also set-option :produce-unsat-assumptions. * define-fun-rec doesn't allow mutual recursion * All options should be restored to defaults with (reset) command. (Currently :incremental and maybe others get "stuck" due to late driver integration.) | |||
2014-10-16 | Add dt.size to datatypes theory. Add option for fairness strategy used by ↵ | ajreynol | |
CEGQI. Improve care graph/equality status for datatypes. Only do FULL effort check in datatypes if no other theories used output channel. | |||
2014-10-10 | Cleanup | Morgan Deters | |
2014-10-10 | Add owner map to better manage QuantifiersModules. Initial infrastructure ↵ | ajreynol | |
for cegqi. | |||
2014-10-08 | Add unsat cores support to CVC native language. | Morgan Deters | |