cvc5.git
8 years agoAdd a few more regressions.
ajreynol [Fri, 12 Aug 2016 17:47:54 +0000 (12:47 -0500)]
Add a few more regressions.

8 years agoMinor fixes to model construction to take singleton equivalence classes into account...
ajreynol [Fri, 12 Aug 2016 17:09:45 +0000 (12:09 -0500)]
Minor fixes to model construction to take singleton equivalence classes into account (fixes sets+dt model bug). Minor fix for mixed int/real quantifier instantiation.

8 years agoMerge pull request #90 from 4tXJ7f/fewer_preproc_holes
guykatzz [Fri, 12 Aug 2016 14:48:43 +0000 (07:48 -0700)]
Merge pull request #90 from 4tXJ7f/fewer_preproc_holes

Add support for fewer preprocessing holes

8 years agoAdd support for fewer preprocessing holes
Andres Notzli [Wed, 10 Aug 2016 02:24:28 +0000 (19:24 -0700)]
Add support for fewer preprocessing holes

This commit adds support for the --fewer-preprocessing-holes flag. This
flag changes the preprocessing part in proofs in two ways: it (1)
removes assertions that are just restating inputs and uses the inputs
directly instead and it (2) changes the form of the preprocessed
assertions to contain the input that they originate from.

The code in this commit is mostly taken from the proofs branch in Guy's
fork.

8 years agoMinor change to strings, introduce proxy vars only when necessary.
ajreynol [Thu, 11 Aug 2016 14:03:47 +0000 (09:03 -0500)]
Minor change to strings, introduce proxy vars only when necessary.

8 years agoImprovements to strings: work on propagations for reverse normal form processing...
ajreynol [Wed, 10 Aug 2016 22:36:45 +0000 (17:36 -0500)]
Improvements to strings: work on propagations for reverse normal form processing. Better handling of disequalities, constant splitting and neg contain approximation. Introduce proxy vars for replace. Refactoring.

8 years agoMerge pull request #89 from 4tXJ7f/fix_proof_spaces
guykatzz [Tue, 9 Aug 2016 21:17:23 +0000 (14:17 -0700)]
Merge pull request #89 from 4tXJ7f/fix_proof_spaces

Fix missing/redundant spaces in proofs

8 years agoFixes for sep star rewrite.
ajreynol [Tue, 9 Aug 2016 18:11:07 +0000 (13:11 -0500)]
Fixes for sep star rewrite.

8 years agoFix missing/redundant spaces in proofs
Andres Notzli [Tue, 9 Aug 2016 03:33:24 +0000 (20:33 -0700)]
Fix missing/redundant spaces in proofs

Before, in some cases, e.g. when printing sorts and in resolution
proofs, the proofs contained redundant and/or missing spaces. With this
commit, CVC4 now prints out `(trust_f (= (Array Index Element) let10
let12)` instead of `(trust_f (= (Array Index  Element )let10 let12))`.

8 years agoMerge pull request #88 from 4tXJ7f/fix_comments
guykatzz [Sat, 6 Aug 2016 06:23:23 +0000 (23:23 -0700)]
Merge pull request #88 from 4tXJ7f/fix_comments

Minor: add/fix comments, remove redundant includes

8 years agoMinor: add/fix comments, remove redundant includes
Andres Notzli [Thu, 4 Aug 2016 22:12:54 +0000 (15:12 -0700)]
Minor: add/fix comments, remove redundant includes

8 years agoFixed an issue where arrays proofs would sometimes have an extra ")" at the end.
Guy [Wed, 3 Aug 2016 22:51:22 +0000 (15:51 -0700)]
Fixed an issue where arrays proofs would sometimes have an extra ")" at the end.

8 years agoMerge pull request #87 from 4tXJ7f/fix_oob_access
barrettcw [Wed, 3 Aug 2016 20:59:04 +0000 (13:59 -0700)]
Merge pull request #87 from 4tXJ7f/fix_oob_access

Fix out-of-bounds access in ExprManager

8 years agoPrioritize inferences when processing normal forms in strings.
ajreynol [Sat, 30 Jul 2016 14:44:42 +0000 (09:44 -0500)]
Prioritize inferences when processing normal forms in strings.

8 years agoThe "aggressive" optimizer for lemma L now returns the conjunction of all lemmas...
Guy [Thu, 28 Jul 2016 20:40:36 +0000 (13:40 -0700)]
The "aggressive" optimizer for lemma L now returns the conjunction of all lemmas L' that originated from L and were used in the unsat core

8 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
Guy [Thu, 28 Jul 2016 18:24:59 +0000 (11:24 -0700)]
Merge branch 'master' of https://github.com/CVC4/CVC4

8 years agoBug fix involving negated lemmas
Guy [Thu, 28 Jul 2016 18:24:07 +0000 (11:24 -0700)]
Bug fix involving negated lemmas

8 years agoFix bug 749.
ajreynol [Thu, 28 Jul 2016 16:21:59 +0000 (11:21 -0500)]
Fix bug 749.

8 years agoAdd the negative conjunction case
Guy [Thu, 28 Jul 2016 16:01:52 +0000 (09:01 -0700)]
Add the negative conjunction case

8 years agoFix out-of-bounds access in ExprManager
Andres Notzli [Wed, 27 Jul 2016 21:06:56 +0000 (14:06 -0700)]
Fix out-of-bounds access in ExprManager

The size of `d_exprStatisticsVars` was `LAST_TYPE` which was not enough
because the INC_STAT macro tries to access
`d_exprStatisticsVars[LAST_TYPE]` in some cases, resulting in an
out-of-bounds access. Found bug with UBSan.

8 years agoProper instrumentation of the preprocessing phase
Guy [Thu, 28 Jul 2016 02:03:13 +0000 (19:03 -0700)]
Proper instrumentation of the preprocessing phase

8 years agoproper handling of ITEs
Guy [Thu, 28 Jul 2016 01:17:41 +0000 (18:17 -0700)]
proper handling of ITEs

8 years agoProper handling of IFF lemmas in the unsat core.
Guy [Wed, 27 Jul 2016 21:27:05 +0000 (14:27 -0700)]
Proper handling of IFF lemmas in the unsat core.
Don't return duplicates in the unsat core

8 years agoAdded an option for a more aggressive weakest implicant optimization
Guy [Wed, 27 Jul 2016 19:54:29 +0000 (12:54 -0700)]
Added an option for a more aggressive weakest implicant optimization

8 years agoIf we can't find a weaker implicant, fail gracefully and return the original lemma
Guy [Wed, 27 Jul 2016 16:46:24 +0000 (09:46 -0700)]
If we can't find a weaker implicant, fail gracefully and return the original lemma

8 years agoMerge pull request #86 from 4tXJ7f/fix_warnings
guykatzz [Wed, 27 Jul 2016 05:07:35 +0000 (22:07 -0700)]
Merge pull request #86 from 4tXJ7f/fix_warnings

Fix warnings in src/proof

8 years agoFix warnings in src/proof
Andres Notzli [Wed, 27 Jul 2016 04:07:24 +0000 (21:07 -0700)]
Fix warnings in src/proof

Fix warning due to `ProofLetCount` being defined as `struct` in
`proof_utils.h` and `class` in `proof.h`. Fix warnings due to different
number of arguments of `printConstantDisequalityProof()` and
`printTheoryLemmaProof()` in subclasses.

8 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
Guy [Tue, 26 Jul 2016 23:38:06 +0000 (16:38 -0700)]
Merge branch 'master' of https://github.com/CVC4/CVC4

8 years agoBug fix:
Guy [Tue, 26 Jul 2016 23:37:57 +0000 (16:37 -0700)]
Bug fix:
If a lemma (a disjunction) has a "false" literal in it, it can be ignored, but a "true" literal really should stay

8 years agoAdd option to minimize sygus solutions based on using weakest implicants of instantia...
ajreynol [Tue, 26 Jul 2016 22:55:09 +0000 (17:55 -0500)]
Add option to minimize sygus solutions based on using weakest implicants of instantiations in unsat cores.

8 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
Guy [Tue, 26 Jul 2016 22:03:37 +0000 (15:03 -0700)]
Merge branch 'master' of https://github.com/CVC4/CVC4

8 years agoLetification of BV constants
Guy [Tue, 26 Jul 2016 22:03:27 +0000 (15:03 -0700)]
Letification of BV constants

8 years agoMinor improvements to strings related to constant splitting, including a few options...
ajreynol [Tue, 26 Jul 2016 20:15:46 +0000 (15:15 -0500)]
Minor improvements to strings related to constant splitting, including a few options (disabled by default).

8 years agoAdded functionality to retrieve a lemma's "weakest implicant" in the unsat core....
Guy [Tue, 26 Jul 2016 20:09:31 +0000 (13:09 -0700)]
Added functionality to retrieve a lemma's "weakest implicant" in the unsat core. Currently, lemmas that are not conjunctions and their own weakest implicants; but for lemmas that *are* conjunctions, we may return only a subset of the conjuncts.

8 years agoBug fix
Guy [Tue, 26 Jul 2016 00:24:39 +0000 (17:24 -0700)]
Bug fix

8 years agoPropagate the usage of proof let maps into constant disequality proofs
Guy [Tue, 26 Jul 2016 00:20:14 +0000 (17:20 -0700)]
Propagate the usage of proof let maps into constant disequality proofs

8 years agoBug fix
Guy [Mon, 25 Jul 2016 23:52:27 +0000 (16:52 -0700)]
Bug fix

8 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
Guy [Mon, 25 Jul 2016 22:59:49 +0000 (15:59 -0700)]
Merge branch 'master' of https://github.com/CVC4/CVC4

8 years agocleanup
Guy [Mon, 25 Jul 2016 06:24:40 +0000 (23:24 -0700)]
cleanup

8 years agoUse letification for the aliasing declarations as well (consequently, print the globa...
Guy [Mon, 25 Jul 2016 05:35:05 +0000 (22:35 -0700)]
Use letification for the aliasing declarations as well (consequently, print the global let map before the aliasing part)

8 years agoProper handling for lemmas that are conjuncts:
Guy [Mon, 25 Jul 2016 03:56:08 +0000 (20:56 -0700)]
Proper handling for lemmas that are conjuncts:
Record a separate recipe for each conjunct, but have as the "original lemma" in this recipe the complete conjunction, so that we can report this to the theory solver later, if asked.

Refactoring: instead of propagating the proof recipes from the theory engine to the prop engine and cnf stream to be registered there, just register them at the theory engine - as the prop engine and cnf stream don't change them.

8 years agoMinor, error handling for polymorphism + sep logic.
ajreynol [Fri, 22 Jul 2016 15:59:16 +0000 (10:59 -0500)]
Minor, error handling for polymorphism + sep logic.

8 years agoFixes for strings, explanations for constant split propagations, substr under concat...
ajreynol [Thu, 21 Jul 2016 15:56:09 +0000 (10:56 -0500)]
Fixes for strings, explanations for constant split propagations, substr under concat rewrite. Avoid duplicate re.range length lemmas.

8 years agoInfrastructure for storing and printing heap models for separation logic. Ensure...
ajreynol [Wed, 20 Jul 2016 18:28:01 +0000 (13:28 -0500)]
Infrastructure for storing and printing heap models for separation logic. Ensure value of sep.nil is correct in models. Print instantiations as sexprs.

8 years agoPrint only instantiations that are in the unsat core when --proof is enabled. Add...
ajreynol [Wed, 20 Jul 2016 16:52:37 +0000 (11:52 -0500)]
Print only instantiations that are in the unsat core when --proof is enabled.  Add option to minimize sygus solutions based on unsat core (disabled by default).

8 years agoInfer conflicts in strings based on abstracting equality as contains. Minor cleanup.
ajreynol [Wed, 20 Jul 2016 16:08:11 +0000 (11:08 -0500)]
Infer conflicts in strings based on abstracting equality as contains. Minor cleanup.

8 years agoBug fix
Guy [Wed, 20 Jul 2016 02:33:15 +0000 (19:33 -0700)]
Bug fix

8 years agoAllow a caller to query whether an unsat core is available or not
Guy [Wed, 20 Jul 2016 02:13:01 +0000 (19:13 -0700)]
Allow a caller to query whether an unsat core is available or not

8 years agoAdd infrastructure for tracking instantiation lemmas (for proofs, and minimization...
ajreynol [Tue, 19 Jul 2016 15:32:37 +0000 (10:32 -0500)]
Add infrastructure for tracking instantiation lemmas (for proofs, and 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.

8 years agoRefactor strings extf evaluation info. Ensure strings eager preprocess eliminates...
ajreynol [Sat, 16 Jul 2016 14:03:11 +0000 (09:03 -0500)]
Refactor strings extf evaluation info. Ensure strings eager preprocess eliminates all extf symbols during ppRewrite. Add options stringGuessModel and stringUfReduct. Minor optimizations.

8 years agoMoved the assertion to a better spot
Guy [Fri, 15 Jul 2016 23:53:54 +0000 (16:53 -0700)]
Moved the assertion to a better spot

8 years agoThe ProofManager now allows theory solvers to get their lemmas that participate in...
Guy [Fri, 15 Jul 2016 23:48:25 +0000 (16:48 -0700)]
The ProofManager now allows theory solvers to get their lemmas that participate in the unsat cores.
Currently this is only limited to lemmas generated via the d_out->lemma() interface, i.e. no propagations
and conflict lemmas.

8 years agoMinor simplification to normal form explanations.
ajreynol [Fri, 15 Jul 2016 14:39:09 +0000 (09:39 -0500)]
Minor simplification to normal form explanations.

8 years agoMinor fix to last commit.
ajreynol [Fri, 8 Jul 2016 11:49:24 +0000 (06:49 -0500)]
Minor fix to last commit.

8 years agoSimplifications for strings normal forms, fix case for concat reps in normal forms.
ajreynol [Fri, 8 Jul 2016 02:03:25 +0000 (21:03 -0500)]
Simplifications for strings normal forms, fix case for concat reps in normal forms.

8 years agoEnsure heap disjointness in sep refinements.
ajreynol [Thu, 7 Jul 2016 22:14:56 +0000 (17:14 -0500)]
Ensure heap disjointness in sep refinements.

8 years agoRefactoring of strings preprocess module. When enabled, apply eager preprocess during...
ajreynol [Thu, 7 Jul 2016 20:22:40 +0000 (15:22 -0500)]
Refactoring of strings preprocess module. When enabled, apply eager preprocess during ppRewrite instead of during processAssertions. Simplify reduction for contains.  Fix bug in explanations for F_EndpointEq. Minor cleanup for sep.

8 years agoA few proof bugs fixed
Guy [Wed, 6 Jul 2016 23:41:33 +0000 (16:41 -0700)]
A few proof bugs fixed

8 years agoMinor cleanup in strings, mostly related to negated str.contains.
ajreynol [Wed, 6 Jul 2016 20:56:10 +0000 (15:56 -0500)]
Minor cleanup in strings, mostly related to negated str.contains.

8 years agoAdd comment field for model, resolves hack for printing sep logic models.
ajreynol [Wed, 6 Jul 2016 18:33:55 +0000 (13:33 -0500)]
Add comment field for model, resolves hack for printing sep logic models.

8 years agoRefactor last call for theories, only create one model when quantifiers are enabled...
ajreynol [Tue, 5 Jul 2016 22:55:25 +0000 (17:55 -0500)]
Refactor last call for theories, only create one model when quantifiers are enabled. Fix sep.nil preregistration in TheorySep.

8 years agoAdd option --trigger-active-sel. Recognize simple triggers with polarity. Do not...
ajreynol [Tue, 5 Jul 2016 20:11:28 +0000 (15:11 -0500)]
Add option --trigger-active-sel. Recognize simple triggers with polarity. Do not drop patterns from merged prenex (fixes bug 743).

8 years agoWhen proving a lemma, ignore literals that don't belong to the theory in question...
Guy [Fri, 1 Jul 2016 23:49:02 +0000 (16:49 -0700)]
When proving a lemma, ignore literals that don't belong to the theory in question, except for equalties

8 years agoHandle bitvector lemmas where a literal gets rewritten into false, and consequently...
Guy [Fri, 1 Jul 2016 21:21:13 +0000 (14:21 -0700)]
Handle bitvector lemmas where a literal gets rewritten into false, and consequently the lemma doesn't match a recorded conflict

8 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
Guy [Thu, 30 Jun 2016 19:39:01 +0000 (12:39 -0700)]
Merge branch 'master' of https://github.com/CVC4/CVC4

8 years agoSupport for the letification of chained AND and OR operations in LFSC proofs
Guy [Thu, 30 Jun 2016 19:38:56 +0000 (12:38 -0700)]
Support for the letification of chained AND and OR operations in LFSC proofs

8 years agoAdd theory/sep/kinds to EXTRA_DIST to fix distcheck failures.
Clark Barrett [Thu, 23 Jun 2016 23:56:49 +0000 (16:56 -0700)]
Add theory/sep/kinds to EXTRA_DIST to fix distcheck failures.

8 years agoFixed some warnings, fixed bug in cdhashmap that was crashing cdmap_black,
Clark Barrett [Thu, 23 Jun 2016 23:55:09 +0000 (16:55 -0700)]
Fixed some warnings, fixed bug in cdhashmap that was crashing cdmap_black,
re-enabled cdmap_black.

8 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
Guy [Mon, 20 Jun 2016 21:20:30 +0000 (14:20 -0700)]
Merge branch 'master' of https://github.com/CVC4/CVC4

8 years agoAddressed a bug that occurs when proof production is triggered via text flags in...
Guy [Mon, 20 Jun 2016 21:20:15 +0000 (14:20 -0700)]
Addressed a bug that occurs when proof production is triggered via text 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

8 years agoMinor change to sep/kinds
ajreynol [Mon, 20 Jun 2016 17:47:04 +0000 (12:47 -0500)]
Minor change to sep/kinds

8 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
Guy [Mon, 20 Jun 2016 17:17:04 +0000 (10:17 -0700)]
Merge branch 'master' of https://github.com/CVC4/CVC4

8 years agoFixed a bug where the proofManager's init() call was not getting called, resutling...
Guy [Mon, 20 Jun 2016 12:40:20 +0000 (05:40 -0700)]
Fixed a bug where the proofManager's init() call was not getting called, resutling a null point deference

8 years agoFix unit test.
ajreynol [Sat, 18 Jun 2016 15:49:21 +0000 (10:49 -0500)]
Fix unit test.

8 years agoCleanup from last commit, treat sep.nil as variable kind.
ajreynol [Fri, 17 Jun 2016 23:38:16 +0000 (18:38 -0500)]
Cleanup from last commit, treat sep.nil as variable kind.

8 years agoSupport for separation logic. Enable cbqi by default for pure BV.
ajreynol [Fri, 17 Jun 2016 20:55:56 +0000 (15:55 -0500)]
Support for separation logic. Enable cbqi by default for pure BV.

8 years agoAdd syguscomp2016 scripts.
ajreynol [Fri, 17 Jun 2016 14:22:09 +0000 (09:22 -0500)]
Add syguscomp2016 scripts.

8 years agoDummy commit.
Clark Barrett [Thu, 9 Jun 2016 18:04:41 +0000 (11:04 -0700)]
Dummy commit.

8 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
Guy [Wed, 8 Jun 2016 22:24:44 +0000 (15:24 -0700)]
Merge branch 'master' of https://github.com/CVC4/CVC4

8 years agoLFSC letification is true by default
Guy [Wed, 8 Jun 2016 18:53:02 +0000 (11:53 -0700)]
LFSC letification is true by default

8 years agoSupport for printing a global let map in LFSC proofs.
Guy [Wed, 8 Jun 2016 18:52:42 +0000 (11:52 -0700)]
Support for printing a global let map in LFSC proofs.
Added a flag to enable/disbale this feature (enabled by default).

Also, added some infrastructure for proving rewrite rules.

8 years agoMerge pull request #85 from CVC4/master_for_proof_merge
guykatzz [Mon, 6 Jun 2016 17:48:50 +0000 (10:48 -0700)]
Merge pull request #85 from CVC4/master_for_proof_merge

Merge from proof branch

8 years agoRemove NodeListMap from datatypes and equality inference. Add option --dt-blast-splits.
ajreynol [Sat, 4 Jun 2016 00:07:05 +0000 (19:07 -0500)]
Remove NodeListMap from datatypes and equality inference. Add option --dt-blast-splits.

8 years agoBetter infrastructure for proving constant disequality.
Guy [Fri, 3 Jun 2016 21:27:00 +0000 (14:27 -0700)]
Better infrastructure for proving constant disequality.
Added support for the BV case

8 years agoA better mechanism for handling BV terms with aliases: inject the alias at the decl_b...
Guy [Fri, 3 Jun 2016 21:10:42 +0000 (14:10 -0700)]
A better mechanism for handling BV terms with aliases: inject the alias at the decl_bblast step, instead of having an individual "with alias" rule for each BV operation

8 years agoRemove NodeListMap from strings, fixes memory leaks. Fix for regexp intersection.
ajreynol [Fri, 3 Jun 2016 19:20:55 +0000 (14:20 -0500)]
Remove NodeListMap from strings, fixes memory leaks. Fix for regexp intersection.

8 years agoSimple memory fixes, minor cleanup in quantifiers.
ajreynol [Fri, 3 Jun 2016 16:39:12 +0000 (11:39 -0500)]
Simple memory fixes, minor cleanup in quantifiers.

8 years agoReduce number of passes in quantifiers rewriter.
ajreynol [Fri, 3 Jun 2016 14:01:30 +0000 (09:01 -0500)]
Reduce number of passes in quantifiers rewriter.

8 years agoFixed a magical bug that only appears when compiling with clang:
Guy [Thu, 2 Jun 2016 21:44:58 +0000 (14:44 -0700)]
Fixed a magical bug that only appears when compiling with clang:
The assignment
      d_exprToVariableName[*it] = assignAlias(*it)

Creates an empty value for *it in d_exprToVariableName, causing the assertion in assignAlias to fail

8 years agoFix
Guy [Thu, 2 Jun 2016 17:17:14 +0000 (10:17 -0700)]
Fix

8 years agoMerge from proof branch
Guy [Thu, 2 Jun 2016 00:46:24 +0000 (17:46 -0700)]
Merge from proof branch

8 years agoRevert "Merging proof branch"
Guy [Thu, 2 Jun 2016 00:41:17 +0000 (17:41 -0700)]
Revert "Merging proof branch"

This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.

8 years agoMerging proof branch
Guy [Thu, 2 Jun 2016 00:33:41 +0000 (17:33 -0700)]
Merging proof branch

8 years agoFix to ignore a case of triggers with no free variables.
ajreynol [Wed, 1 Jun 2016 21:25:50 +0000 (16:25 -0500)]
Fix to ignore a case of triggers with no free variables.

8 years agoInitial infrastructure for bounded set quantification (disabled). Refactoring and...
ajreynol [Wed, 1 Jun 2016 20:51:39 +0000 (15:51 -0500)]
Initial infrastructure for bounded set quantification (disabled). Refactoring and fixes for --fmf-bound-int. Fix simple memory leaks in strings and bounded integers.

8 years agoAdded Guy to authors list.
Clark Barrett [Tue, 31 May 2016 01:01:14 +0000 (18:01 -0700)]
Added Guy to authors list.

8 years agoFix build
Clark Barrett [Sat, 28 May 2016 17:52:38 +0000 (10:52 -0700)]
Fix build

8 years agoUpdated incremental run script
Clark Barrett [Sat, 28 May 2016 17:28:38 +0000 (10:28 -0700)]
Updated incremental run script

8 years agoDisabling failing unit test for now
Clark Barrett [Sat, 28 May 2016 15:58:44 +0000 (08:58 -0700)]
Disabling failing unit test for now

8 years agoRemoving check that is no longer valid.
Clark Barrett [Sat, 28 May 2016 00:43:40 +0000 (17:43 -0700)]
Removing check that is no longer valid.