Age | Commit message (Collapse) | Author |
|
|
|
The `testMultipleCollection` test case was allocating a
ListenerCollection without deleting it. The helper function
`countCommands` was not deleting the `Command`s returned from
`InteractiveShell::readCommand`. In the `testEmptyFileInput` and
`testSimpleFileInput` tests, the `filename` string was not deleted. This
commit fixes all issues.
|
|
|
|
unbounded heaps in sep logic. Fix another simple memory leak in sygus.
|
|
The `testPushPop()` test case does a pop out of scope at the end that
lead to UB in `ContextManager::pop()` because it did a `deque::back()`
on an empty deque without checking. This commit adds an assertion in the
`ContextManager` and checks that the test case triggers the assertion.
|
|
|
|
Fix a few more memory leaks.
|
|
|
|
Fix TRAVIS_CVC4 + TRAVIS_CVC4_DISTCHECK build
|
|
as extension of sets solver, add regressions.
|
|
This commit adds regress4 to the `test/regress/Makefile.am`.
|
|
|
|
|
|
|
|
This reverts commit 3395c5c13cd61d98aec0d9806e3b9bc3d707968a, reversing
changes made to 5f415d4585134612bc24e9a823289fee35541a01.
|
|
Conflicts:
src/options/quantifiers_options
|
|
A bug was introduced in the cleanup process as preparation for the merge
(theory_sets_private.cpp, lines 2502-2508 in this commit).
|
|
|
|
|
|
|
|
breaking in theory sep.
|
|
|
|
allow sep disequal card constants when type is monotonic. Update logics on sep regressions.
|
|
|
|
|
|
bounded set membership.
|
|
|
|
account (fixes sets+dt model bug). Minor fix for mixed int/real quantifier instantiation.
|
|
processing. Better handling of disequalities, constant splitting and neg contain approximation. Introduce proxy vars for replace. Refactoring.
|
|
|
|
|
|
under concat rewrite. Avoid duplicate re.range length lemmas.
|
|
cleanup.
|
|
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.
|
|
|
|
forms.
|
|
|
|
preprocess during ppRewrite instead of during processAssertions. Simplify reduction for contains. Fix bug in explanations for F_EndpointEq. Minor cleanup for sep.
|
|
enabled. Fix sep.nil preregistration in TheorySep.
|
|
not drop patterns from merged prenex (fixes bug 743).
|
|
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
|
|
re-enabled cdmap_black.
|
|
|
|
|
|
|
|
This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.
|
|
|
|
|
|
Refactoring and fixes for --fmf-bound-int. Fix simple memory leaks in strings and bounded integers.
|
|
|