summaryrefslogtreecommitdiff
path: root/test/regress
AgeCommit message (Collapse)Author
2016-11-11Add simple inferences for extended bitvector functions, add a few related ↵ajreynol
options. Use bv2nat, int2bv as triggers. Add regressions.
2016-11-08Add a few options to separation logic and sets. Minor changes to separation ↵ajreynol
logic, change syntax for empty heap constraint.
2016-11-03Add priorities to getNextDecision. Properly handle case for finite types + ↵ajreynol
unbounded heaps in sep logic. Fix another simple memory leak in sygus.
2016-11-02Add missing regression.ajreynol
2016-11-02Fix bug in separation logic for finite pto-data types. Minor cleanup in sep. ↵ajreynol
Fix a few more memory leaks.
2016-10-26Enable bv2nat regressionsajreynol
2016-10-26Merge pull request #98 from 4tXJ7f/fix_dist_buildAndrew Reynolds
Fix TRAVIS_CVC4 + TRAVIS_CVC4_DISTCHECK build
2016-10-26New implementation of sets+cardinality. Merge Paul Meng's relation solver ↵ajreynol
as extension of sets solver, add regressions.
2016-10-23Fix TRAVIS_CVC4 + TRAVIS_CVC4_DISTCHECK buildAndres Notzli
This commit adds regress4 to the `test/regress/Makefile.am`.
2016-10-21Fix/add missing makefiles.ajreynol
2016-10-21Move slow regress0 benchmarks to regress1, increment regress1 through regress3.ajreynol
2016-10-13Merging bv parts of ajr/bvExt branch, minor additions to ExtTheory.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-10-11Merge branch 'origin' of https://github.com/CVC4/CVC4.gitPaul Meng
Conflicts: src/options/quantifiers_options
2016-09-28Fix the merge of kbansal/card branch (2039eab).Kshitij Bansal
A bug was introduced in the cleanup process as preparation for the merge (theory_sets_private.cpp, lines 2502-2508 in this commit).
2016-09-20More refactoring of cbqi. Add a few regressions. Add option for qcf.ajreynol
2016-09-13refactored the code, added more benchmarks and minor fixesPaul Meng
2016-09-12fixed capitalized "kind"Paul Meng
2016-09-12Ensure sep.nil is unique per type at NodeManager level. Add simple symmetry ↵ajreynol
breaking in theory sep.
2016-09-09Fix bug in unconstrained simplifier related to sep.nil/distinguished variables.ajreynol
2016-09-09Support for separation logic + EPR. Refactor preprocessing of sep.nil, only ↵ajreynol
allow sep disequal card constants when type is monotonic. Update logics on sep regressions.
2016-08-30added more benchmarksPaul Meng
2016-08-24Merge remote-tracking branch 'origin/master'PaulMeng
2016-08-15Enable bounded set membership with --fmf-bound. Map to term models for ↵ajreynol
bounded set membership.
2016-08-12Add a few more regressions.ajreynol
2016-08-12Minor fixes to model construction to take singleton equivalence classes into ↵ajreynol
account (fixes sets+dt model bug). Minor fix for mixed int/real quantifier instantiation.
2016-08-10Improvements to strings: work on propagations for reverse normal form ↵ajreynol
processing. Better handling of disequalities, constant splitting and neg contain approximation. Introduce proxy vars for replace. Refactoring.
2016-08-09Fixes for sep star rewrite.ajreynol
2016-07-28Fix bug 749.ajreynol
2016-07-21Fixes for strings, explanations for constant split propagations, substr ↵ajreynol
under concat rewrite. Avoid duplicate re.range length lemmas.
2016-07-20Infer conflicts in strings based on abstracting equality as contains. Minor ↵ajreynol
cleanup.
2016-07-19Add infrastructure for tracking instantiation lemmas (for proofs, and ↵ajreynol
minimization of --dump-instantiations, qe and synthesis solutions). Eliminate quantified arithmetic variables that only have lower/upper bounds. Cleanup strings preprocess, minor fix for str.replace semantics. Reorder cegqi before fmf. Minor cleanup.
2016-07-08Minor fix to last commit.ajreynol
2016-07-07Simplifications for strings normal forms, fix case for concat reps in normal ↵ajreynol
forms.
2016-07-07Ensure heap disjointness in sep refinements.ajreynol
2016-07-07Refactoring of strings preprocess module. When enabled, apply eager ↵ajreynol
preprocess during ppRewrite instead of during processAssertions. Simplify reduction for contains. Fix bug in explanations for F_EndpointEq. Minor cleanup for sep.
2016-07-05Refactor last call for theories, only create one model when quantifiers are ↵ajreynol
enabled. Fix sep.nil preregistration in TheorySep.
2016-07-05Add option --trigger-active-sel. Recognize simple triggers with polarity. Do ↵ajreynol
not drop patterns from merged prenex (fixes bug 743).
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-17Support for separation logic. Enable cbqi by default for pure BV.ajreynol
2016-06-01Merge from proof branchGuy
2016-06-01Revert "Merging proof branch"Guy
This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.
2016-06-01Merging proof branchGuy
2016-06-01Fix to ignore a case of triggers with no free variables.ajreynol
2016-06-01Initial infrastructure for bounded set quantification (disabled). ↵ajreynol
Refactoring and fixes for --fmf-bound-int. Fix simple memory leaks in strings and bounded integers.
2016-05-26Use term indexing in TheoryUF::computeCareGraph. Do not reject model value ↵ajreynol
instantiations in cbqi+BV. Use dag in alpha equivalence check. Fix simple memory leak in fmf.
2016-05-23Fix related to parametric sorts whose interpretation is finite due to ↵ajreynol
uninterpreted sorts + FMF. Generalizes previous fix in term registration visitor.
2016-05-21Minor fix for strings.ajreynol
2016-05-20Minor fix to strings, cleanup in datatypes.ajreynol
2016-05-18Refactor modes for sygus+single invocation. Add option --inst-rlv-cond. ↵ajreynol
Minor fixes for inst max level.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback