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

8 years agoMinor fix cbqi for constant monomials.
ajreynol [Tue, 17 May 2016 17:52:44 +0000 (12:52 -0500)]
Minor fix cbqi for constant monomials.

8 years agoFix memory leak in interactive_shell.cpp
Clark Barrett [Mon, 16 May 2016 20:27:57 +0000 (13:27 -0700)]
Fix memory leak in interactive_shell.cpp

8 years agoEnable --sygus-direct-eval by default, limit to terms that do not induce Boolean...
ajreynol [Mon, 16 May 2016 22:30:59 +0000 (17:30 -0500)]
Enable --sygus-direct-eval by default, limit to terms that do not induce Boolean structure.  Minor fixes for bitvectors: rewrite SDIV to total operators when options::bitvectorDivByZeroConst is true, fix collectModelInfo when fullModel=false. Lift ITEs in sygus search. Fix sygus initialization related to cbqi.

8 years agoWork on --sygus-direct-eval. Minor optimizations, updates to casc scripts. Enable...
ajreynol [Sun, 15 May 2016 17:34:51 +0000 (12:34 -0500)]
Work on --sygus-direct-eval. Minor optimizations, updates to casc scripts. Enable e-matching when --strings-exp is enabled.

8 years agoAdd casc scripts. Improvements to qcf related to nested quantifiers and variable...
ajreynol [Thu, 12 May 2016 15:13:17 +0000 (10:13 -0500)]
Add casc scripts. Improvements to qcf related to nested quantifiers and variable ordering.

8 years agoFix for --inst-max-level
ajreynol [Tue, 10 May 2016 20:10:10 +0000 (15:10 -0500)]
Fix for --inst-max-level

8 years agoAdd smt comp 2016 scripts. Fix for --relevant-triggers. Add minor optimizations to...
ajreynol [Tue, 10 May 2016 19:33:08 +0000 (14:33 -0500)]
Add smt comp 2016 scripts. Fix for --relevant-triggers. Add minor optimizations to sygus and qcf.

8 years agoRe-enabling ite simplification in incremental mode - no reason why
Clark Barrett [Mon, 9 May 2016 22:21:22 +0000 (15:21 -0700)]
Re-enabling ite simplification in incremental mode - no reason why
it should be a problem.

8 years agoMinor clean up, fixes related to sygus.
ajreynol [Fri, 6 May 2016 22:04:52 +0000 (17:04 -0500)]
Minor clean up, fixes related to sygus.

8 years agoCompute term indices lazily in TermDb. Optimization for qcf to recognize irrelevant...
ajreynol [Thu, 5 May 2016 23:44:47 +0000 (18:44 -0500)]
Compute term indices lazily in TermDb. Optimization for qcf to recognize irrelevant quantifiers based on irrelevant functions. Fix rewriter for prefix merges.  Minor optimizations for LFSC. Work on --literal-matching. Updates to inst propagate, move instantiation filtering within qe. Enable sygus for string inputs.

8 years agoRemoving a null pointer reference that was found by -fsanitize=null.
Tim King [Thu, 5 May 2016 17:35:04 +0000 (10:35 -0700)]
Removing a null pointer reference that was found by -fsanitize=null.

8 years agoUpdate to COPYING
Clark Barrett [Thu, 5 May 2016 04:30:13 +0000 (21:30 -0700)]
Update to COPYING

8 years agoClean up issues related to compiled scc in LFSC. Refactor --partial-trigger, do not...
ajreynol [Mon, 2 May 2016 14:16:30 +0000 (09:16 -0500)]
Clean up issues related to compiled scc in LFSC. Refactor --partial-trigger, do not combine quantifier prefixes with annotations. Eliminate use of context-dependent attributes in quantifiers.

8 years agoReviewed Tim's Asan changes and improved SatProof comments.
Liana Hadarean [Sat, 30 Apr 2016 16:57:43 +0000 (09:57 -0700)]
Reviewed Tim's Asan changes and improved SatProof comments.

8 years agoWorkaround for a problem in clang
Clark Barrett [Thu, 28 Apr 2016 21:39:35 +0000 (17:39 -0400)]
Workaround for a problem in clang

8 years agoMore work on inst propagate. Optimization for qcf to check instances eagerly. Improv...
ajreynol [Thu, 28 Apr 2016 12:01:05 +0000 (07:01 -0500)]
More work on inst propagate.  Optimization for qcf to check instances eagerly. Improvements to equality query for disequalities.

8 years agoAdding an example lsan supression file.
Tim King [Wed, 27 Apr 2016 19:54:29 +0000 (12:54 -0700)]
Adding an example lsan supression file.

8 years agoFixing memory leaks for garbage collection of ResChains in the sat proof implementati...
Tim King [Tue, 26 Apr 2016 21:51:04 +0000 (14:51 -0700)]
Fixing memory leaks for garbage collection of ResChains in the sat proof implementation. As a part of tracking this down, I've modified a number of accessor functions in TSatProof to be const. An expert in this code will need to do a pass over this.

8 years agoFixing a memory leak of the ProofManager.
Tim King [Tue, 26 Apr 2016 17:52:15 +0000 (10:52 -0700)]
Fixing a memory leak of the ProofManager.

8 years agoFixed typo
Clark Barrett [Tue, 19 Apr 2016 16:01:14 +0000 (09:01 -0700)]
Fixed typo

8 years agoMore fixes for python interface
Clark Barrett [Mon, 18 Apr 2016 23:06:45 +0000 (16:06 -0700)]
More fixes for python interface

8 years agoRolling back the rewrite code
Guy [Fri, 15 Apr 2016 22:34:52 +0000 (15:34 -0700)]
Rolling back the rewrite code

8 years agoFix for bug 717
Clark Barrett [Fri, 15 Apr 2016 21:54:15 +0000 (14:54 -0700)]
Fix for bug 717

8 years agoFixes for python bindings
Clark Barrett [Fri, 15 Apr 2016 20:31:55 +0000 (13:31 -0700)]
Fixes for python bindings

8 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
Guy [Thu, 14 Apr 2016 23:05:25 +0000 (16:05 -0700)]
Merge branch 'master' of https://github.com/CVC4/CVC4

8 years agoRemove some no-longer-required rewrites of array lemmas
Guy [Thu, 14 Apr 2016 23:04:57 +0000 (16:04 -0700)]
Remove some no-longer-required rewrites of array lemmas

8 years agoAdd option --snorm-infer-eq to infer equalities based on normalization in ArithCongru...
ajreynol [Thu, 14 Apr 2016 16:38:51 +0000 (11:38 -0500)]
Add option --snorm-infer-eq to infer equalities based on normalization in ArithCongruenceManager at standard effort (disabled by default).

8 years agoAdd missing function for regexp to expr manager.
ajreynol [Thu, 14 Apr 2016 15:28:34 +0000 (10:28 -0500)]
Add missing function for regexp to expr manager.

8 years agoUpdate native language support for strings.
ajreynol [Wed, 13 Apr 2016 21:29:01 +0000 (16:29 -0500)]
Update native language support for strings.

8 years agoMinor improvements for alpha equivalence and partial quantifier elimination in increm...
ajreynol [Wed, 13 Apr 2016 20:02:31 +0000 (15:02 -0500)]
Minor improvements for alpha equivalence and partial quantifier elimination in incremental mode. Change defaults to addInstantiation method.

8 years agoHandle parametric datatypes with --quant-ind. Minor updates.
ajreynol [Wed, 13 Apr 2016 16:22:43 +0000 (11:22 -0500)]
Handle parametric datatypes with --quant-ind. Minor updates.

8 years agoBug fixes related to parametric datatypes + theory combination + quantifiers. Add...
ajreynol [Tue, 12 Apr 2016 21:29:20 +0000 (16:29 -0500)]
Bug fixes related to parametric datatypes + theory combination + quantifiers. Add regression.

8 years agoOptimizations for QCF to check relevant domain of variable argument positions eagerly...
ajreynol [Tue, 12 Apr 2016 15:13:45 +0000 (10:13 -0500)]
Optimizations for QCF to check relevant domain of variable argument positions eagerly, global ordering mechanism for quantified formulas within check. Refactoring of term database.

8 years agoMinor fixes for inst match generators. Updates to qip.
ajreynol [Mon, 11 Apr 2016 14:17:06 +0000 (09:17 -0500)]
Minor fixes for inst match generators. Updates to qip.

8 years agoMore work on instantiation propagation. Enable external filtering of instantiations...
ajreynol [Sun, 10 Apr 2016 20:20:33 +0000 (15:20 -0500)]
More work on instantiation propagation. Enable external filtering of instantiations. All quantifiers strategies terminate when a conflict can be established.

8 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
Guy [Sat, 9 Apr 2016 20:05:50 +0000 (13:05 -0700)]
Merge branch 'master' of https://github.com/CVC4/CVC4

8 years agoMade ProofArray's printing functions non-static, and consequently the data members...
Guy [Sat, 9 Apr 2016 20:05:14 +0000 (13:05 -0700)]
Made ProofArray's printing functions non-static, and consequently the data members non-static as well

8 years agocardinality operation for finite sets (based on my thesis / ijcar16 paper)
Kshitij Bansal [Tue, 3 Nov 2015 09:47:30 +0000 (04:47 -0500)]
cardinality operation for finite sets (based on my thesis / ijcar16 paper)

Some further cleanup/fixes pending

This is squash of 39 commits (kbansal/card branch + cleanup):
* add card operator
* local reasoning
* towards graph building
* first implementation
* close cardinality terms
* model building
* more
* more
* more
* Add aggressive sets rewriting.
* Recursively aggressive rewrite sets.
* Fix
* incomplete card2 implementation
* ...
* Avoid using auto in sets.
* fix merge
* more
* ...
* more
* ...
* Fixed for loops
* Slight modification to computeRelevantTerms
* more
* ..
* more
* ...
* mv empty set lemma generation to later point
* more options/reordering
* debug related
* more trace
* ...
* fix merge_nodes, models
* rm warnigns
* fix compile errors
* warning
* bug fixes/cleanup
* mroe fixes
* cleanup
* ...

8 years agoMinor refactoring of entailment tests and quantifiers util. Initial draft of instanti...
ajreynol [Sat, 9 Apr 2016 18:07:11 +0000 (13:07 -0500)]
Minor refactoring of entailment tests and quantifiers util. Initial draft of instantiation propagator.

8 years agoRefactor trigger selection, revisions to --relational-trigger. Properly process non...
ajreynol [Thu, 7 Apr 2016 14:38:41 +0000 (09:38 -0500)]
Refactor trigger selection, revisions to --relational-trigger. Properly process non-standard user-provided triggers. Avoid entailed instantiations based on equality earlier. Refactor core addInstantiation method, add notification mechanism. Add optional argument to entailment checks. Fix bug for duplicate triggers.

8 years agoNew options for trigger selection, add option --strict-triggers. Do not infer alpha...
ajreynol [Mon, 4 Apr 2016 22:18:36 +0000 (17:18 -0500)]
New options for trigger selection, add option --strict-triggers. Do not infer alpha equivalence for quantifiers with annotations, limit rewrite operations when triggers are trusted.

8 years agoUpdating the copyright headers and scripts.
Tim King [Mon, 4 Apr 2016 02:38:06 +0000 (19:38 -0700)]
Updating the copyright headers and scripts.

8 years agos_ prefix for static members
Guy [Mon, 4 Apr 2016 03:12:19 +0000 (20:12 -0700)]
s_ prefix for static members

8 years agoRemoved the theory-specific merge reason types. Instead, added a mechanism for dynami...
Guy [Sun, 3 Apr 2016 22:58:58 +0000 (15:58 -0700)]
Removed the theory-specific merge reason types. Instead, added a mechanism for dynamically allocating these tags upon request.

8 years agoImprovements to equality inference module: add missing cases for solvable variables...
ajreynol [Fri, 1 Apr 2016 21:42:56 +0000 (16:42 -0500)]
Improvements to equality inference module: add missing cases for solvable variables, do not infer equalities that are derivable by transitivity of other inferred equalities, refactor solved vars/eqc into one, option to track explanations.  Handle case when equality inference in quantifiers can derive purely arithmetic ground conflicts at full effort.