cvc5.git
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.

8 years agoMerged QF_UFBV support from experimental branch
Clark Barrett [Fri, 27 May 2016 21:40:20 +0000 (14:40 -0700)]
Merged QF_UFBV support from experimental branch

8 years agoEnabled bit-blasting option for QF_UFBV
Clark Barrett [Fri, 27 May 2016 21:28:24 +0000 (14:28 -0700)]
Enabled bit-blasting option for QF_UFBV

8 years agoUpdated incremental script
Clark Barrett [Fri, 27 May 2016 06:26:12 +0000 (23:26 -0700)]
Updated incremental script

8 years agoFixed bug in run script
Clark Barrett [Fri, 27 May 2016 04:03:39 +0000 (21:03 -0700)]
Fixed bug in run script

8 years agoAdded cryptominisat flag to QF_NIA
Kshitij Bansal [Thu, 26 May 2016 23:18:59 +0000 (19:18 -0400)]
Added cryptominisat flag to QF_NIA

8 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
Clark Barrett [Thu, 26 May 2016 23:15:16 +0000 (16:15 -0700)]
Merge branch 'master' of https://github.com/CVC4/CVC4

8 years agoSmall change in run script
Clark Barrett [Thu, 26 May 2016 23:12:14 +0000 (16:12 -0700)]
Small change in run script

8 years agoChanged aig_bitblaster to work with cryptominisat
lianah [Thu, 26 May 2016 23:05:01 +0000 (19:05 -0400)]
Changed aig_bitblaster to work with cryptominisat

8 years agoDisabled m4ri in cryptominisat cmake command
lianah [Thu, 26 May 2016 22:35:34 +0000 (18:35 -0400)]
Disabled m4ri in cryptominisat cmake command

8 years agoFix for aig_bitblaster.cpp
Kshitij Bansal [Thu, 26 May 2016 22:19:51 +0000 (18:19 -0400)]
Fix for aig_bitblaster.cpp

8 years agoUse term indexing in TheoryUF::computeCareGraph. Do not reject model value instantiat...
ajreynol [Thu, 26 May 2016 19:51:01 +0000 (14:51 -0500)]
Use term indexing in TheoryUF::computeCareGraph. Do not reject model value instantiations in cbqi+BV. Use dag in alpha equivalence check. Fix simple memory leak in fmf.

8 years agoUpdated script, fixed bug in QF_NIA conversion.
Clark Barrett [Thu, 26 May 2016 19:41:05 +0000 (12:41 -0700)]
Updated script, fixed bug in QF_NIA conversion.

8 years agoFixed unit test
Liana Hadarean [Wed, 25 May 2016 07:03:53 +0000 (00:03 -0700)]
Fixed unit test

8 years agoFixed build issue due to dummy Cryptominisat constructor.
Liana Hadarean [Wed, 25 May 2016 06:16:06 +0000 (23:16 -0700)]
Fixed build issue due to dummy Cryptominisat constructor.

8 years agoForgot to add second patch file.
Liana Hadarean [Wed, 25 May 2016 05:36:14 +0000 (22:36 -0700)]
Forgot to add second patch file.

8 years agoMerged cryptominisat from experimental branch.
Liana Hadarean [Wed, 25 May 2016 05:30:41 +0000 (22:30 -0700)]
Merged cryptominisat from experimental branch.

8 years agoImprovements to symmetry breaking in sygus search. Minor fix for getting instantiatio...
ajreynol [Tue, 24 May 2016 23:18:00 +0000 (18:18 -0500)]
Improvements to symmetry breaking in sygus search. Minor fix for getting instantiations of non-registered quantifiers in sygus.

8 years agoFix related to parametric sorts whose interpretation is finite due to uninterpreted...
ajreynol [Mon, 23 May 2016 19:28:29 +0000 (14:28 -0500)]
Fix related to parametric sorts whose interpretation is finite due to uninterpreted sorts + FMF.  Generalizes previous fix in term registration visitor.

8 years agoMinor fix for strings.
ajreynol [Sat, 21 May 2016 21:58:19 +0000 (16:58 -0500)]
Minor fix for strings.

8 years agoMinor fix to strings, cleanup in datatypes.
ajreynol [Fri, 20 May 2016 22:10:03 +0000 (17:10 -0500)]
Minor fix to strings, cleanup in datatypes.

8 years agoImprovements to theory combination + strings: do not return trivial care graph, split...
ajreynol [Fri, 20 May 2016 18:59:13 +0000 (13:59 -0500)]
Improvements to theory combination + strings: do not return trivial care graph, split on length terms for disequal strings. Term indexing for TheoryDatatypes::computeCareGraph. Minor fix in quantifiers rewriter for entailed conditions, strings cardinality.

8 years agoUpdated AUTHORS file
Clark Barrett [Fri, 20 May 2016 12:58:06 +0000 (05:58 -0700)]
Updated AUTHORS file

8 years agoRefactor modes for sygus+single invocation. Add option --inst-rlv-cond. Minor fixes...
ajreynol [Wed, 18 May 2016 15:06:49 +0000 (10:06 -0500)]
Refactor modes for sygus+single invocation.  Add option --inst-rlv-cond. Minor fixes for inst max level.