summaryrefslogtreecommitdiff
path: root/src/parser/smt2/smt2.h
AgeCommit message (Collapse)Author
2018-08-08Plug solver API object into parser. (#2240)Aina Niemetz
2018-07-14sygusComp2018: update semantics for declare-fun in sygus. (#2102)Andrew Reynolds
2018-06-25Updated copyright headers.Aina Niemetz
2018-06-04Only enable transcendentals if logic is N[I]RAT (#2052)Andres Noetzli
2018-05-29 Make user's SMT2 version override file version (#2004)Andres Noetzli
2018-05-29Track input language in a single place (#2003)Andres Noetzli
2018-05-02Initial support for string standard in smt lib 2.6 (#1848)Andrew Reynolds
2018-03-05Enable -Wsuggest-override by default. (#1643)Mathias Preiner
Adds missing override keywords.
2018-01-06Removing throw specifiers from src/parser/. (#1486)Tim King
2017-12-06Add command for define-fun-rec and add to API (#1412)Andrew Reynolds
2017-11-23Ho parsing and regressions (#1350)Andrew Reynolds
2017-11-22Sygus Lambda Grammars (#1390)Andrew Reynolds
2017-10-11Move unsat core names to smt engine (#1192)Andrew Reynolds
* Move unsat core names to SmtEnginePrivate. Adds a SetExpressionNameCommand to do this. Removes the names field from GetUnsatCoreCommand. * Comment * Pass expression names by reference. * Update throw specifiers. * Minor * Switch expression names to CDMap, simplify interface for printing unsat core names. * Revert throw specifier change. * Minor simplifcations
2017-10-03Op overload parser (#1162)Andrew Reynolds
* Update parser for operator overloading. * Improvements * Updates * Add assert
2017-07-20Moving from the gnu extensions for hash maps to the c++11 hash mapsTim King
* Replacing __gnu_cxx::hash_map with std::unordered_map. * Replacing __gnu_cxx::hash_set with std::unordered_set. * Replacing __gnu_cxx::hash with std::hash. * Adding missing includes.
2017-07-10Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes ↵ajreynol
decision procedure to share selectors of the same type across multiple constructors. Major rewrite of the SyGuS solver. Adds several new strategies for I/O example problems (PBE) and invariant synthesis. Major simplifications to sygus parsing and synthesis conjecture representation. Do not support check-synth in portfolio. Add sygus regressions.
2017-07-07Update copyright headers.Mathias Preiner
2017-03-16Parsing support for SMT LIB 2.6. Minor fixes for printing datatypes. Fix for ↵ajreynol
mkGroundTerm for parametric datatypes. Minor change to run_regression to allow regressions to override input language. Minor refactoring to Cvc.g.
2016-11-13Adding garbage collection for the Smt2 Parser for Commands when exceptions ↵Tim King
are thrown.
2016-11-01Revert change to datatypes API for passing pointers, instead make deep copy ↵ajreynol
during call to mkMutualDatatypes.
2016-11-01Working memory leak free version, changes interface to pointers.ajreynol
2016-06-17Support for separation logic. Enable cbqi by default for pure BV.ajreynol
2016-04-03Updating the copyright headers and scripts.Tim King
2016-01-28Adding listeners to Options.Tim King
- Options -- Added the new option attribute :notify. One can get a notify() call on the Listener after a the option's value is updated. This is the new preferred way to achieve dynamic dispatch for options. -- Removed SmtOptionsHandler and pushed its functionality into OptionsHandler and Listeners. -- Added functions to Options for registering listeners of the notify calls. -- Changed a number of options to use the new listener infrastructure. -- Fixed a number of warnings in options. -- Added the ArgumentExtender class to better capture how arguments are inserted while parsing options and ease memory management. Previously this was the "preemptGetopt" procedure. -- Moved options/options_handler_interface.{cpp,h} to options/options_handler.{cpp,h}. - Theories -- Reimplemented alternative theories to use a datastructure stored on TheoryEngine instead of on Options. - Ostream Handling: -- Added new functionality that generalized how ostreams are opened, options/open_stream.h. -- Simplified the memory management for different ostreams, smt/managed_ostreams.h. -- Had the SmtEnginePrivate manage the memory for the ostreams set by options. -- Simplified how the setting of ostreams are updated, smt/update_ostream.h. - Configuration and Tags: -- Configuration can now be used during predicates and handlers for options. -- Moved configuration.{cpp,h,i} and configuration_private.h from util/ into base/. -- Moved {Debug,Trace}_tags.* from being generated in options/ into base/. - cvc4_private.h -- Upgraded #warning's in cvc4_private.h and cvc4_private_library.h to #error's. -- Added public first-order (non-templatized) member functions for options get and set the value of options outside of libcvc4. Fixed all of the use locations. -- Made lib/lib/clock_gettime.h a cvc4_private_library.h header. - Antlr -- Fixed antlr and cvc4 macro definition conflicts that caused warnings. - SmtGlobals -- Refactored replayStream and replayLog out of SmtGlobals. -- Renamed SmtGlobals to LemmaChannels and moved the implementation into smt_util/lemma_channels.{h,cpp}.
2015-07-31Sygus support for inductive datatypes.ajreynol
2015-07-20Squashed merge of SygusComp 2015 branch.ajreynol
2015-06-11Handle duplicate operators in sygus grammars. Parse sygus quoted literals. ↵ajreynol
Add regression.
2015-06-11Update experimental scripts. Support top-level non-terminals in sygus ↵ajreynol
grammars. Allow -N in sygus terms. Minor bug fix in datatypes_sygus. Add regression.
2015-06-10Support for printing solutions involving LetGTerm sygus. Bug fix define-fun ↵ajreynol
within LetGTerm sygus. Bug fix sygus argument generalization. Add regressions.
2015-06-10Parse support for sygus LetGTerm.ajreynol
2015-06-03Refactoring of sygus parsing, properly parse Constant/Variable constructors.ajreynol
2015-05-11Allow sygus with no syntactic restrictions for LIA. Add regressions.ajreynol
2015-05-11Support for arbitrary constants/variables in Sygus grammars.ajreynol
2015-01-20Handle miniscoping of conjunctions in synthesis properties. Refactor ↵ajreynol
construction of sygus datatypes. Expand define-fun in evaluators.
2015-01-16Linearize multiplication by constants in sygus grammars. Handle unary minus ↵ajreynol
integer numerals. Refactor to smt2.cpp.
2015-01-16Allow uninterpreted/defined functions in Sygus grammars. Fix bug regarding ↵ajreynol
declare-var vs synth-fun arguments. Handle ground properties in sythesis conjectures.
2015-01-14sygus input language and benchmarkMorgan Deters
2014-12-03Floating point infrastructure.Martin Brain
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
2014-10-23Parsing 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-08-26Improved SMT-LIBv2 language support for unsat cores.Morgan Deters
2014-08-22Unsat core infrastruture and API (SMT-LIB compliance to come).Morgan Deters
2014-07-01Update copyrights.Morgan Deters
2014-06-04SMT strict mode now disallows N-ary use of concat, bvadd, bvmul, bvand, ↵Morgan Deters
bvor, and bvxor.
2014-03-19Minor usability fixes related to SMT-LIB compliance.Morgan Deters
2014-03-05Don't tokenize SET_THEORY operators in smt2 parserKshitij Bansal
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-09-11Theory of strings.Tianyi Liang
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
2013-06-19Give a more useful parse error message for "undeclared variable -1".Morgan Deters
Indeed, "-1" is a valid user symbol in SMT-LIB; this commit makes a small change to the parser to detect when something like "-1" is used but undeclared, and adds a note to the error message giving the syntax for unary minus.
2013-06-04File inclusion in Smt2 parser.Morgan Deters
The extended command (include-file "filename") now includes file content.
2013-05-28Standardize SMT-LIBv2 set of logics to use LogicInfo.Morgan Deters
Previously, SMT-LIB logics were treated specially, as in SMT-LIB v1.2. This led to inconsistencies---such as nonstandard logics like "QF_LIRA" being accepted in set-logic but not providing the "Real" sort. Now, the LogicInfo is used and queried, so nonstandard logics should work fine and declare the correct symbols. SMT-LIB v1.2, unfortunately, can't take advantage of this fully since symbols like "Array" have substantially different meanings in different logics.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback