summaryrefslogtreecommitdiff
path: root/src/parser
AgeCommit message (Collapse)Author
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-07-07Use new copyright header format.Mathias Preiner
2017-07-05Non-linear supported in ALL logics. Minor fixes for set logic with sygus.ajreynol
2017-06-30Minor change to trigger selection, fixes related to subtypes (in macros, ↵ajreynol
cbqi, tptp parser), fix full saturation instantiation to not loop in rare case, update regressions, update casc scripts.
2017-06-16Fix stream parsingAndres Nötzli
This commit fixes bug 811. Bug 811 was caused because tokens were referring to a buffer that was reallocated and thus the pointers were not valid anymore. Background: The buffered input stream avoids copying the whole input stream before handing it to ANTLR (in contrast to the non-buffered input stream that first copies everything into a buffer). This enables interactivity (e.g. with kind2) and may save memory. CVC4 uses it when reading from stdin in competition mode for the application track (the incremental benchmarks) and in non-competition mode. To set the CVC4_SMTCOMP_APPLICATION_TRACK flag, the {C,CXX}FLAGS have to be modified at configure time. Solution: This commit fixes the issue by changing how a stream gets buffered. Instead of storing the stream into a single buffer, CVC4 now stores each line in a separate buffer, making sure that they do not have to move, keeping tokens valid. The commit adds the LineBuffer class for managing those buffers. It further modifies CVC4's LA and consume functions to use line number and position within a line to index into the line buffer. This allows us to use the standard mark()/etc. functions because they automatically store and restore that state. The solution also (arguably) simplifies the code. Disadvantages: Tokens split across lines would cause problems (seems reasonable to me). One allocation per line. Alternatives considered: Pull request 162 by Tim was a first attempt to solve the problem. The issues with this solution are: memory usage (old versions of the buffer do not get deleted), tokens split across buffers would be problematic, and mark()/rewind()/etc. would have to be overwritten for the approach to work. I had a partially working fix that used indexes into the stream instead of pointers to memory. The solution stored the content of the stream into a segmented buffer (lines were not guaranteed to be consecutive in memory. This approach was working for basic use cases but had the following issues: ugly casting (the solution requires casting the index to a pointer and storing it in the input stream's nextChar because that's where ANTLR is taking the location information from when creating a token), more modifications (not only would this solution require overwriting more functions of the input stream such as substr, it also requires changes to the use of GETCHARINDEX() in the Smt2 parser and AntlrInput::tokenText() for example), more complex code.
2017-06-16Parse 'is', 'match' differently for non-DT inputAndres Noetzli
In SMT 2.6, Datatypes are being introduced and they come with testers (indexed identifier of the form (_ is c)) and match expressions. This lead to failures in UFIDL benchmarks in SMT-LIB because they declare the function 'is'. This commit changes the parser s.t. it does not consider 'is' and 'match' special tokens unless the theory of datatypes is enabled.
2017-05-16Avoid tokenizing FP tokens in non-FP inputAndres Noetzli
This commit addresses bug 807. CVC4 was parsing floating-point related tokens such as NaN as floating-point tokens even for inputs that do not use the FP theory, which lead to failing SMT-LIB benchmarks that declare functions named NaN.
2017-04-28Minor fixesajreynol
2017-04-24Fix parsing selectors for nullary constructors in smtlib 2.6 format.ajreynol
2017-04-20Support for relational operators identity and join imagePaul Meng
2017-04-12Add nullary operator metakind.ajreynol
2017-03-22Work on new approach for sygus involving conditional solutions. Refactoring ↵ajreynol
of sygus solver. Bug fix for sygus solution reconstruction.
2017-03-20fixed cvc4 parser for set complementPaul Meng
2017-03-16More fixes, features to examples.ajreynol
2017-03-16Minor fixes, always expand applications of lambdas at preprocess.ajreynol
2017-03-16Support for SMT LIB 2.6 syntax declare-datatype and match.ajreynol
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-15Allow 0 argument recursive functions. Fixes bug 782.ajreynol
2017-03-07More fixes for printing/parsing sets, fix kind name.ajreynol
2017-03-07Fix cvc parser for set compliment.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-12-07Added cardinality to cvc language, fixes bug 753. Throw logic exception when ↵ajreynol
using cardinality on sets with finite element type.
2016-11-30Fix parsing of BVROTR by CVC parserAndres Notzli
This commit fixes Bugzilla bug 766 as proposed by jacobly.alt@gmail.com.
2016-11-18Add support for set-logic ALL, fix compiler error in GCC 6.1Clark Barrett
2016-11-13Adding garbage collection for the Smt2 Parser for Commands when exceptions ↵Tim King
are thrown.
2016-11-12Merge pull request #107 from timothy-king/smt1-parser-exception-leaksClark Barrett
Adding garbage collection for the Smt1 Parser for Commands when…
2016-11-12Adding garbage collection for the Smt1 Parser for Commands when exceptions ↵Tim King
are thrown.
2016-11-11Adding garbage collection for the CVC Parser for Commands when exceptions ↵Tim King
are thrown.
2016-11-11Deleting the remaining commands in the Parser's queue within ~Parser().Tim King
2016-11-11Applying clang-format to parser.cpp.Tim King
2016-11-09Fix tptp parser memory leaks for include.ajreynol
2016-11-02Fix a few obvious memory leaks in sygus and quantifiers. Minor fix cvc3_compat.ajreynol
2016-11-01Revert change to Datatypes API to return vector of DatatypeTypes, as before. ↵ajreynol
ASAN failures with datatypes should now be mostly fixed.
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-10-26New implementation of sets+cardinality. Merge Paul Meng's relation solver ↵ajreynol
as extension of sets solver, add regressions.
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-10-11Merge branch 'origin' of https://github.com/CVC4/CVC4.gitPaul Meng
Conflicts: src/options/quantifiers_options
2016-09-25Closing an open file descriptor in MemoryMapFile.Tim King
2016-09-25Freeing memory in error handling code for bounded_token_buffer.Tim King
2016-09-14Support for unique variable generation in node manager.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-15Work on --sygus-direct-eval. Minor optimizations, updates to casc scripts. ↵ajreynol
Enable e-matching when --strings-exp is enabled.
2016-05-06Minor clean up, fixes related to sygus.ajreynol
2016-05-05Compute term indices lazily in TermDb. Optimization for qcf to recognize ↵ajreynol
irrelevant quantifiers based on irrelevant functions. Fix rewriter for prefix merges. Minor optimizations for LFSC. Work on --literal-matching. Updates to inst propagate, move instantiation filtering within qe. Enable sygus for string inputs.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback