summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-07-05fixes bugs in std effort for TCPaulMeng
2016-07-01When proving a lemma, ignore literals that don't belong to the theory in ↵Guy
question, except for equalties
2016-07-01Handle bitvector lemmas where a literal gets rewritten into false, and ↵Guy
consequently the lemma doesn't match a recorded conflict
2016-06-30Merge branch 'master' of https://github.com/CVC4/CVC4Guy
2016-06-30Support for the letification of chained AND and OR operations in LFSC proofsGuy
2016-06-25debug statementPaulMeng
2016-06-25Merge remote-tracking branch 'origin/master'PaulMeng
2016-06-25testPaulMeng
2016-06-25reimplemented std effort for TCPaulMeng
2016-06-23Add theory/sep/kinds to EXTRA_DIST to fix distcheck failures.Clark Barrett
2016-06-23Fixed some warnings, fixed bug in cdhashmap that was crashing cdmap_black,Clark Barrett
re-enabled cdmap_black.
2016-06-20Merge branch 'master' of https://github.com/CVC4/CVC4Guy
2016-06-20Addressed a bug that occurs when proof production is triggered via text ↵Guy
flags in the input. Separated some initialization into two phases: 1. Those that can be done when the proof compiliation flag is set 2. Those that can be done only when the --proof option is set. For #2, deferred their execution until the text flags in the input have been processed
2016-06-20Minor change to sep/kindsajreynol
2016-06-20Merge branch 'master' of https://github.com/CVC4/CVC4Guy
2016-06-20Fixed a bug where the proofManager's init() call was not getting called, ↵Guy
resutling a null point deference
2016-06-18Fix unit test.ajreynol
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-06-17Add syguscomp2016 scripts.ajreynol
2016-06-09Dummy commit.Clark Barrett
2016-06-08Merge branch 'master' of https://github.com/CVC4/CVC4Guy
2016-06-08LFSC letification is true by defaultGuy
2016-06-08Support for printing a global let map in LFSC proofs.Guy
Added a flag to enable/disbale this feature (enabled by default). Also, added some infrastructure for proving rewrite rules.
2016-06-06Merge pull request #85 from CVC4/master_for_proof_mergeguykatzz
Merge from proof branch
2016-06-03Remove NodeListMap from datatypes and equality inference. Add option ↵ajreynol
--dt-blast-splits.
2016-06-03Better infrastructure for proving constant disequality.Guy
Added support for the BV case
2016-06-03A better mechanism for handling BV terms with aliases: inject the alias at ↵Guy
the decl_bblast step, instead of having an individual "with alias" rule for each BV operation
2016-06-03Remove NodeListMap from strings, fixes memory leaks. Fix for regexp ↵ajreynol
intersection.
2016-06-03Simple memory fixes, minor cleanup in quantifiers.ajreynol
2016-06-03Reduce number of passes in quantifiers rewriter.ajreynol
2016-06-02Fixed a magical bug that only appears when compiling with clang:Guy
The assignment d_exprToVariableName[*it] = assignAlias(*it) Creates an empty value for *it in d_exprToVariableName, causing the assertion in assignAlias to fail
2016-06-02FixGuy
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-30Added Guy to authors list.Clark Barrett
2016-05-28Fix buildClark Barrett
2016-05-28Updated incremental run scriptClark Barrett
2016-05-28Disabling failing unit test for nowClark Barrett
2016-05-27Removing check that is no longer valid.Clark Barrett
2016-05-27Merged QF_UFBV support from experimental branchClark Barrett
2016-05-27Enabled bit-blasting option for QF_UFBVClark Barrett
2016-05-26Updated incremental scriptClark Barrett
2016-05-26Fixed bug in run scriptClark Barrett
2016-05-26Added cryptominisat flag to QF_NIAKshitij Bansal
2016-05-26Merge branch 'master' of https://github.com/CVC4/CVC4Clark Barrett
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback