summaryrefslogtreecommitdiff
path: root/src/printer/smt2
AgeCommit message (Collapse)Author
2018-03-09Add support for SMT-LIB v2.5 command get-unsat-assumptions (#1653)Aina Niemetz
2018-03-05Add support for check-sat-assuming. (#1637)Aina Niemetz
This adds support for check-sat-assuming. It further adds support for SmtEngine::query() over a vector of Expressions, e.g., smtEngine->query({a, b}); checks the validity (of the current input formula) under assumption (not (or a b)).
2018-02-07Add remaining transcendental functions (#1551)Andrew Reynolds
2018-02-05Cleaning up the printing of theory model representative sets. (#1538)Tim King
2017-12-27Rel smt parser (#1446)Arjun Viswanathan
2017-12-06Add command for define-fun-rec and add to API (#1412)Andrew Reynolds
2017-11-28Removing throw specifiers from internal Printer hierarchy. (#1393)Tim King
2017-11-22Converting defined functions and let expressions from Sygus grammars to ↵Haniel Barbosa
lambdas (#1403) This partially solves issue #1344. Definitions are expanded when the grammar normalizer is called. When this becomes default then the code that expands definitions elsewhere will be removed. The PR also contains minor changes to the PrintCallback and SygusGrammarNormalize module.
2017-11-22Sygus Lambda Grammars (#1390)Andrew Reynolds
2017-11-15Sygus print callbacks (#1348)Andrew Reynolds
* Initial infrastructure for sygus printing. * Minor * Minor improvements * Format * Minor * Empty constructor printer. * Format * Minor * Format * Address.
2017-11-10Printing for higher-order (#1347)Andrew Reynolds
2017-11-09Higher-order prep (#1338)Andrew Reynolds
* Minor preparation for final higher-order merge. * Format
2017-10-27Refactor theory model (#1236)Andrew Reynolds
* Refactor theory model, working on making RepSet references const. * Encapsulation of members of rep set. * More documentation on rep set. * Swap names * Reference issues. * Minor * Minor * New clang format.
2017-10-18Strings API escape sequences (#1245)Andrew Reynolds
* Argument for strings class to specify whether to process escape sequences. * Change default value on string constructor. * Make CVC4::String::toString symmetric to the constructor for CVC4::String, document. * Clang format.
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-09Split term database (#1206)Andrew Reynolds
* Move equality query to own file, move equality inference to quantifiers engine. * Move quantifiers attributes out of TermDb and into QuantAttribute. * Move term database sygus to quantifiers engine, move some attributes to quantifiers attributes header. * Split term database into term util. * Partial fix for #1205 that eliminates need for dependency in node.cpp. * Add more references to github issues.
2017-10-02Add 5 FP kinds for partial to total fn conversion (#1128)Martin
- Add new kinds for partially defined functions - Print the new kinds - Type rules for the new total kinds - Constant folding and rewrites for the new total kinds
2017-09-19Fix issue #1074, improve non-fatal error handling (#1075)Andres Noetzli
Commit 54d24c786d6a843cc72dfb5e377603349ea5e420 was changing CVC4 to handle certain non-fatal errors (such as calling get-unsat-core without a proceding unsat check-sat command) without terminating the solver. In the case of get-unsat-cores, the changes lead to the solver crashing because it was trying to print an unsat core initialized with the default constructor, so the member variable d_smt was NULL, which lead to a dereference of a null pointer. One of the issues of the way non-fatal errors were handled was that the error reporting was done in the invoke() method of the command instead of the printResult() method, which lead to the error described above and other issues such as a call to get-value printing a value after reporting an error. This commit aims to improve the design by adding a RecoverableModalException for errors that the solver can recover from and CommandRecoverableFailure to communicate that a command failed in a way that does not prohibit the solver from continuing to execute. The exception RecoverableModalException is thrown by the SMTEngine and the commands catch it and turn it into a CommandRecoverableFailure. The commit changes all error conditions from the commit above and adds a regression test for them.
2017-09-18Floating point symfpu support (#1103)Martin
- Update the parser to the new constant construction - Fix the problem with parsing +/-zero and remove some dead code - Extend the interface for literal floating-point values. - Add a constructor so that a parameteric operator structure can be created from a type - Add constructors so parametric operator constants can be easily converted - Update SMT2 printing so that it uses the informative output
2017-09-05Remove support for conversions between uint32/uint16 and string. (#1069)Andrew Reynolds
* Remove support for conversions between uint32/uint16 and string. * Temporarily disable regression.
2017-07-12Make type rules more strict for operators whose type rules involve subtypes. ↵ajreynol
Disable support for subrange and predicate subtypes (which were only partially supported previously).
2017-07-10Merge ntExt branch. Adds support for transcendental functions. Refactoring ↵ajreynol
of non-linear extension. Add factoring lemma scheme for non-linear. Add regressions.
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-06-21Properly handle subtypes in smt2 printer.ajreynol
2017-05-30print only labeled assertions as part of the unsat coreguykatzz
added the option dump-unsat-cores-full for printing the entire core, as before
2017-05-25Quote unsat core names if applicable, fixes bug 816.ajreynol
2017-04-20Minor fixes.ajreynol
2017-04-14Fix nullary operator printers, minor.ajreynol
2017-04-02Adding a model based axiom instantiation scheme for multiplication. Merge ↵Tim King
commit for nlAlgMaster.
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.
2017-03-07More fixes for printing/parsing sets, fix kind name.ajreynol
2017-03-06Support for set compliment and universe set. Simplify approach for sep.nil ↵ajreynol
nodes.
2017-03-02Eliminate Boolean term conversion. Generalizes removeITE pass to remove ↵ajreynol
Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
2017-01-04Fix for tff type declarations inTPTP parser, fixes bug 748. Other minor ↵ajreynol
changes.
2016-11-22Fix smt2 and cvc printers for testers when output and input languages are ↵ajreynol
different.
2016-11-01Working memory leak free version, changes interface to pointers.ajreynol
2016-10-13Revert "Merge branch 'origin' of https://github.com/CVC4/CVC4.git"Tim King
This reverts commit 3395c5c13cd61d98aec0d9806e3b9bc3d707968a, reversing changes made to 5f415d4585134612bc24e9a823289fee35541a01.
2016-08-24Merge remote-tracking branch 'origin/master'PaulMeng
2016-07-20Infrastructure for storing and printing heap models for separation logic. ↵ajreynol
Ensure value of sep.nil is correct in models. Print instantiations as sexprs.
2016-07-06Add comment field for model, resolves hack for printing sep logic models.ajreynol
2016-07-05Merge branch 'master' of https://github.com/CVC4/CVC4.gitPaulMeng
Conflicts: proofs/signatures/Makefile.am src/Makefile.am src/expr/datatype.cpp src/options/datatypes_options src/options/options_template.cpp src/options/quantifiers_options src/proof/arith_proof.cpp src/proof/arith_proof.h src/proof/array_proof.cpp src/proof/array_proof.h src/proof/bitvector_proof.cpp src/proof/bitvector_proof.h src/proof/cnf_proof.cpp src/proof/cnf_proof.h src/proof/proof_manager.cpp src/proof/proof_manager.h src/proof/sat_proof.h src/proof/sat_proof_implementation.h src/proof/skolemization_manager.h src/proof/theory_proof.cpp src/proof/theory_proof.h src/proof/uf_proof.cpp src/proof/uf_proof.h src/prop/cnf_stream.cpp src/prop/cnf_stream.h src/prop/minisat/core/Solver.cc src/prop/prop_engine.cpp src/prop/prop_engine.h src/prop/theory_proxy.cpp src/smt/smt_engine.cpp src/smt/smt_engine_check_proof.cpp src/theory/arrays/array_proof_reconstruction.cpp src/theory/arrays/theory_arrays.cpp src/theory/bv/eager_bitblaster.cpp src/theory/bv/lazy_bitblaster.cpp src/theory/datatypes/theory_datatypes.cpp src/theory/quantifiers/alpha_equivalence.cpp src/theory/quantifiers/candidate_generator.cpp src/theory/quantifiers/candidate_generator.h src/theory/quantifiers/ce_guided_single_inv.cpp src/theory/quantifiers/ceg_instantiator.cpp src/theory/quantifiers/conjecture_generator.cpp src/theory/quantifiers/equality_infer.cpp src/theory/quantifiers/equality_infer.h src/theory/quantifiers/inst_match_generator.cpp src/theory/quantifiers/inst_propagator.cpp src/theory/quantifiers/inst_propagator.h src/theory/quantifiers/inst_strategy_e_matching.cpp src/theory/quantifiers/inst_strategy_e_matching.h src/theory/quantifiers/instantiation_engine.cpp src/theory/quantifiers/model_builder.cpp src/theory/quantifiers/model_engine.cpp src/theory/quantifiers/quant_conflict_find.cpp src/theory/quantifiers/quant_conflict_find.h src/theory/quantifiers/quant_split.cpp src/theory/quantifiers/quant_util.cpp src/theory/quantifiers/quantifiers_rewriter.cpp src/theory/quantifiers/quantifiers_rewriter.h src/theory/quantifiers/term_database.cpp src/theory/quantifiers/term_database.h src/theory/quantifiers/trigger.cpp src/theory/quantifiers/trigger.h src/theory/quantifiers_engine.cpp src/theory/quantifiers_engine.h src/theory/sets/kinds src/theory/sets/theory_sets_private.cpp src/theory/sets/theory_sets_private.h src/theory/sets/theory_sets_rewriter.cpp src/theory/sets/theory_sets_type_rules.h src/theory/strings/theory_strings.cpp src/theory/strings/theory_strings.h src/theory/theory_engine.cpp src/theory/theory_engine.h src/theory/uf/equality_engine.cpp test/regress/regress0/fmf/Makefile.am test/regress/regress0/quantifiers/Makefile.am test/regress/regress0/strings/Makefile.am test/regress/regress0/sygus/Makefile.am test/regress/regress0/sygus/max2-univ.sy
2016-06-17Cleanup from last commit, treat sep.nil as variable kind.ajreynol
2016-06-17Support for separation logic. Enable cbqi by default for pure BV.ajreynol
2016-05-06Minor clean up, fixes related to sygus.ajreynol
2016-04-20update from the masterPaulMeng
2016-04-15change transitive closure operator name to TCLOUSREPaulMeng
2016-04-09cardinality operation for finite sets (based on my thesis / ijcar16 paper)Kshitij Bansal
Some further cleanup/fixes pending This is squash of 39 commits (kbansal/card branch + cleanup): * add card operator * local reasoning * towards graph building * first implementation * close cardinality terms * model building * more * more * more * Add aggressive sets rewriting. * Recursively aggressive rewrite sets. * Fix * incomplete card2 implementation * ... * Avoid using auto in sets. * fix merge * more * ... * more * ... * Fixed for loops * Slight modification to computeRelevantTerms * more * .. * more * ... * mv empty set lemma generation to later point * more options/reordering * debug related * more trace * ... * fix merge_nodes, models * rm warnigns * fix compile errors * warning * bug fixes/cleanup * mroe fixes * cleanup * ...
2016-04-03Updating the copyright headers and scripts.Tim King
2016-03-23squash-merge from proof branchGuy
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback