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

8 years agoImprovements to trigger selection, min triggers by default. Optimizations for E-match...
ajreynol [Thu, 31 Mar 2016 19:36:25 +0000 (14:36 -0500)]
Improvements to trigger selection, min triggers by default. Optimizations for E-matching. Minor work to equality infer.

8 years agoUpdates to E-matching to avoid entailed instantiations earlier. Minor updates to...
ajreynol [Wed, 30 Mar 2016 19:06:27 +0000 (14:06 -0500)]
Updates to E-matching to avoid entailed instantiations earlier. Minor updates to datatypes lemmas, other minor changes.

8 years agoUpdating the mailmap for git.
Tim King [Wed, 30 Mar 2016 16:15:43 +0000 (09:15 -0700)]
Updating the mailmap for git.

8 years agoMinor cleanup from last commit (quant util, equality infer). Do not set fmfBoundIntLa...
ajreynol [Mon, 28 Mar 2016 21:26:57 +0000 (16:26 -0500)]
Minor cleanup from last commit (quant util, equality infer). Do not set fmfBoundIntLazy for stringsExp.

8 years agoImplement equality inference module for arithmetic terms. Optimization for entailmen...
ajreynol [Mon, 28 Mar 2016 17:32:58 +0000 (12:32 -0500)]
Implement equality inference module for arithmetic terms.  Optimization for entailment checks.  Other minor infrastructure.

8 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
Guy [Thu, 24 Mar 2016 23:56:31 +0000 (16:56 -0700)]
Merge branch 'master' of https://github.com/CVC4/CVC4

8 years agoRefactored the equality engine in order to remove theory-specific logic from equality...
Guy [Thu, 24 Mar 2016 23:56:13 +0000 (16:56 -0700)]
Refactored the equality engine in order to remove theory-specific logic from equality path reconstruction

8 years agoFixing a garbage collection issue in simplifyWithCare(). Bug 729.
Tim King [Thu, 24 Mar 2016 22:06:24 +0000 (15:06 -0700)]
Fixing a garbage collection issue in simplifyWithCare(). Bug 729.

8 years agoDeleting allocated NodeVecs in ITESimplifier.
Tim King [Thu, 24 Mar 2016 21:58:13 +0000 (14:58 -0700)]
Deleting allocated NodeVecs in ITESimplifier.

8 years agoFreeing CegConjecture::d_ceg_si. Also making d_ceg_si a provate member of CegConjecture.
Tim King [Thu, 24 Mar 2016 20:12:49 +0000 (13:12 -0700)]
Freeing CegConjecture::d_ceg_si. Also making d_ceg_si a provate member of CegConjecture.

8 years agoFixing a memory leak in CDInstMatchTrie::d_data.
Tim King [Thu, 24 Mar 2016 18:21:31 +0000 (11:21 -0700)]
Fixing a memory leak in CDInstMatchTrie::d_data.

8 years agoFix for a memory leak in InstStrategyCegqi.
Tim King [Thu, 24 Mar 2016 17:54:00 +0000 (10:54 -0700)]
Fix for a memory leak in InstStrategyCegqi.

8 years agoFixing a memory leak in QuantInfo::d_var_mg.
Tim King [Thu, 24 Mar 2016 17:44:05 +0000 (10:44 -0700)]
Fixing a memory leak in QuantInfo::d_var_mg.

8 years agoMerge pull request #82 from CVC4/master_for_merge
guykatzz [Wed, 23 Mar 2016 19:12:10 +0000 (12:12 -0700)]
Merge pull request #82 from CVC4/master_for_merge

Squash-merge from the proof branch

8 years agosquash-merge from proof branch
Guy [Wed, 23 Mar 2016 19:07:59 +0000 (12:07 -0700)]
squash-merge from proof branch

8 years agoFixing memory leaks in Trigger and TriggerTrie.
Tim King [Wed, 23 Mar 2016 18:12:04 +0000 (11:12 -0700)]
Fixing memory leaks in Trigger and TriggerTrie.

8 years agoFixed help for tear-down-incremental option
Clark Barrett [Wed, 23 Mar 2016 17:15:36 +0000 (10:15 -0700)]
Fixed help for tear-down-incremental option

8 years agoFixing two garbage collection issues in Region and SortModel.
Tim King [Wed, 23 Mar 2016 07:56:12 +0000 (00:56 -0700)]
Fixing two garbage collection issues in Region and SortModel.

8 years agoDeleting the CDInstMatchTries in QuantifiersEngine::d_c_inst_match_trie.
Tim King [Wed, 23 Mar 2016 04:22:15 +0000 (21:22 -0700)]
Deleting the CDInstMatchTries in QuantifiersEngine::d_c_inst_match_trie.

8 years agoGarbage collecting the EqcInfo s in TheoryDatatypes::d_eqc_info.
Tim King [Wed, 23 Mar 2016 04:09:55 +0000 (21:09 -0700)]
Garbage collecting the EqcInfo s in TheoryDatatypes::d_eqc_info.

8 years agoGarbage collecting the MinisatEmptyNotify for the EagerBitblaster.
Tim King [Wed, 23 Mar 2016 03:45:14 +0000 (20:45 -0700)]
Garbage collecting the MinisatEmptyNotify for the EagerBitblaster.

8 years agoBug fix for define functions + incremental. Minor work on relational triggers.
ajreynol [Tue, 22 Mar 2016 19:07:21 +0000 (14:07 -0500)]
Bug fix for define functions + incremental. Minor work on relational triggers.

8 years agoDeleting the contents of d_modelGlobalsCommands before it is cleared.
Tim King [Tue, 22 Mar 2016 05:16:45 +0000 (22:16 -0700)]
Deleting the contents of d_modelGlobalsCommands before it is cleared.

8 years agoNew version of the recursive options parsing strategy.
Tim King [Tue, 22 Mar 2016 03:51:07 +0000 (20:51 -0700)]
New version of the recursive options parsing strategy.

8 years agoLimit duplicate propagating instances to avoid exponential behavior in QuantConflictFind.
ajreynol [Fri, 18 Mar 2016 15:05:32 +0000 (10:05 -0500)]
Limit duplicate propagating instances to avoid exponential behavior in QuantConflictFind.

8 years agoChange internal representative selection for finite domains that do not involve unint...
ajreynol [Wed, 16 Mar 2016 18:57:53 +0000 (13:57 -0500)]
Change internal representative selection for finite domains that do not involve uninterpreted sorts, including bounded integer quantification.

8 years agoAdd options related to interleaving quantifiers and theory combination, changes defau...
ajreynol [Sat, 12 Mar 2016 16:38:36 +0000 (10:38 -0600)]
Add options related to interleaving quantifiers and theory combination, changes default behavior.

8 years agoFaster conditional rewriting for and/or beneath quantifiers. Improvements to sort...
ajreynol [Thu, 10 Mar 2016 23:49:13 +0000 (17:49 -0600)]
Faster conditional rewriting for and/or beneath quantifiers. Improvements to sort inference, related to constants. Add several quantifiers options, minor refactoring.

8 years agoExtend synthesis solver to handle single invocation with additional universal quantif...
ajreynol [Tue, 8 Mar 2016 18:10:41 +0000 (12:10 -0600)]
Extend synthesis solver to handle single invocation with additional universal quantification. Refactor query/check-sat to call one internal function in SmtEngine. Make check-synth its own command. Minor work on quant ee.

8 years agoMinor change to F-Length inference in strings. No internal tracking of cardinality...
ajreynol [Mon, 7 Mar 2016 18:39:50 +0000 (12:39 -0600)]
Minor change to F-Length inference in strings. No internal tracking of cardinality assertions in uf. Change fullModel false array collectModelInfo to assign constants.

8 years agoAdd missing code to track dependencies recursively for string explanations as well.
ajreynol [Thu, 3 Mar 2016 16:02:34 +0000 (10:02 -0600)]
Add missing code to track dependencies recursively for string explanations as well.

8 years agoWork towards complete instantiation for datatypes.
ajreynol [Wed, 2 Mar 2016 19:54:07 +0000 (13:54 -0600)]
Work towards complete instantiation for datatypes.

8 years agoShorter explanations for strings based on tracking which parts of normal forms are...
ajreynol [Tue, 1 Mar 2016 22:29:14 +0000 (16:29 -0600)]
Shorter explanations for strings based on tracking which parts of normal forms are dependent upon which equalities. Add anti-skolemization module to quantifiers. Disable rewriting of non-clashing equalities between same constructors.

8 years agoMinor options to datatypes.
ajreynol [Mon, 29 Feb 2016 16:04:20 +0000 (10:04 -0600)]
Minor options to datatypes.

8 years agoRefactoring of inferences in strings. Add several options.
ajreynol [Fri, 26 Feb 2016 19:39:06 +0000 (13:39 -0600)]
Refactoring of inferences in strings. Add several options.

8 years agoMinor improvement to partial qe. Add options for representative selection in FMF.
ajreynol [Thu, 25 Feb 2016 16:10:47 +0000 (10:10 -0600)]
Minor improvement to partial qe. Add options for representative selection in FMF.

8 years agoAdd entailment checks between length terms to reduce splitting in strings solver...
ajreynol [Wed, 24 Feb 2016 18:19:09 +0000 (12:19 -0600)]
Add entailment checks between length terms to reduce splitting in strings solver.  Minor additions to datatypes and qcf.

8 years agoAdding the missing clause_id.h file.
Tim King [Wed, 24 Feb 2016 18:39:39 +0000 (10:39 -0800)]
Adding the missing clause_id.h file.

8 years agoUnifying the definitions of ClauseId to a single source of truth.
Tim King [Wed, 24 Feb 2016 08:19:12 +0000 (00:19 -0800)]
Unifying the definitions of ClauseId to a single source of truth.

8 years agoFix term database for non-equal, congruent terms in master equality engine. Disable...
ajreynol [Tue, 23 Feb 2016 17:33:09 +0000 (11:33 -0600)]
Fix term database for non-equal, congruent terms in master equality engine. Disable ITE terms in quant conflict find.

8 years agoFixes and improvements for datatypes properties and splitting.
ajreynol [Fri, 19 Feb 2016 17:00:48 +0000 (11:00 -0600)]
Fixes and improvements for datatypes properties and splitting.

8 years agoImplement dynamic splitting for quantified formulas. Minor refactoring of reductions...
ajreynol [Fri, 19 Feb 2016 04:50:05 +0000 (22:50 -0600)]
Implement dynamic splitting for quantified formulas.  Minor refactoring of reductions in quantifiers engine.

8 years agoCorrect subtyping for arrays, disable subtyping for predicate subtypes. Bug fixes...
ajreynol [Thu, 18 Feb 2016 21:21:34 +0000 (15:21 -0600)]
Correct subtyping for arrays, disable subtyping for predicate subtypes.  Bug fixes in quantifiers related to subtypes/parametric sorts.  Make macros trace dependencies for get-unsat-core. Add regressions.

8 years agofix for windows builds
Kshitij Bansal [Thu, 18 Feb 2016 03:58:01 +0000 (22:58 -0500)]
fix for windows builds

8 years agoRefactor quantifiers attributes. Make quantifier elimination robust to preprocessing...
ajreynol [Wed, 17 Feb 2016 23:35:56 +0000 (17:35 -0600)]
Refactor quantifiers attributes. Make quantifier elimination robust to preprocessing, implement get-qe-disjunct.

8 years agoPublic interface for quantifier elimination. Minor changes to datatypes rewriter.
ajreynol [Tue, 16 Feb 2016 20:55:28 +0000 (14:55 -0600)]
Public interface for quantifier elimination.  Minor changes to datatypes rewriter.

8 years agoMore simplification to internal implementation of tuples and records.
ajreynol [Tue, 16 Feb 2016 00:10:42 +0000 (18:10 -0600)]
More simplification to internal implementation of tuples and records.

8 years agoMinor change to last commit
ajreynol [Mon, 15 Feb 2016 19:38:51 +0000 (13:38 -0600)]
Minor change to last commit

8 years agoEliminate most of the internal representation infrastructure for tuples and records...
ajreynol [Mon, 15 Feb 2016 19:02:02 +0000 (13:02 -0600)]
Eliminate most of the internal representation infrastructure for tuples and records, replace with datatypes throughout, update cvc printer for tuples/records.  Minor changes to API for records and tuples.

8 years agoMore aggressive conditional rewriting for quantified formulas. Bug fix set incomplete...
ajreynol [Thu, 11 Feb 2016 21:07:37 +0000 (15:07 -0600)]
More aggressive conditional rewriting for quantified formulas. Bug fix set incomplete for fmc.

8 years agoFix model postprocessor for tuples, add regression.
ajreynol [Wed, 10 Feb 2016 16:17:18 +0000 (10:17 -0600)]
Fix model postprocessor for tuples, add regression.

8 years agoFix regression, minor change to output.
ajreynol [Tue, 9 Feb 2016 22:57:50 +0000 (16:57 -0600)]
Fix regression, minor change to output.

8 years agoEager introduction of eqc, lemma cache for ground fmf. Apply preprocessing to quantif...
ajreynol [Tue, 9 Feb 2016 19:23:18 +0000 (13:23 -0600)]
Eager introduction of eqc, lemma cache for ground fmf. Apply preprocessing to quantifier instantiations.

8 years agoUpdates related to finite model finding and (co)datatypes. Bug fix enumerator and...
ajreynol [Mon, 8 Feb 2016 21:49:14 +0000 (15:49 -0600)]
Updates related to finite model finding and (co)datatypes. Bug fix enumerator and codatatype rewriter, further simplify fmc.

8 years agoChanging the way the equality engine explains disequalities.
guykatzz [Sat, 6 Feb 2016 00:10:36 +0000 (16:10 -0800)]
Changing the way the equality engine explains disequalities.

The explanation for a != b is now:
1. a == find(a)
2. ( find(a) == find(b) ) == false
3. find(b) == b

This simplifies the creation of transitivity proofs for disequalities.

8 years agoAdd two optimizations for datatypes, currently disabled. Bug fix rewriter for selecto...
ajreynol [Fri, 5 Feb 2016 16:24:49 +0000 (10:24 -0600)]
Add two optimizations for datatypes, currently disabled. Bug fix rewriter for selectors applied to codatatype values.

8 years agoFixed two more memory leaks in array_info.cpp
Clark Barrett [Thu, 4 Feb 2016 21:57:26 +0000 (13:57 -0800)]
Fixed two more memory leaks in array_info.cpp

8 years agoAdded --omit-dont-cares option which doesn't print model values for
Clark Barrett [Wed, 3 Feb 2016 22:04:27 +0000 (14:04 -0800)]
Added --omit-dont-cares option which doesn't print model values for
variables known to be don't-cares.

8 years agoMoving dump.*, command.*, model.*, and ite_removal.* from smt_util/ to smt/. Breaking...
Tim King [Tue, 2 Feb 2016 17:47:34 +0000 (09:47 -0800)]
Moving dump.*, command.*, model.*, and ite_removal.* from smt_util/ to smt/. Breaking an edge between the sat solver and command.h.

8 years agoRemoving the CVC4_PUBLIC attribute from the forward declaration of Record in type.h.
Tim King [Mon, 1 Feb 2016 19:45:14 +0000 (11:45 -0800)]
Removing the CVC4_PUBLIC attribute from the forward declaration of Record in type.h.

8 years agoRemoving the CVC4_NEEDS_REPLACEMENT_FUNCTIONS guard to have a simpler build process.
Tim King [Mon, 1 Feb 2016 19:43:31 +0000 (11:43 -0800)]
Removing the CVC4_NEEDS_REPLACEMENT_FUNCTIONS guard to have a simpler build process.

8 years agoGeneralizing lib/strtok_r.c so that it can always be compiled.
Tim King [Mon, 1 Feb 2016 19:29:49 +0000 (11:29 -0800)]
Generalizing lib/strtok_r.c so that it can always be compiled.

8 years agoGeneralizing the implementation of lib/clock_gettime.c so that it can always be compiled.
Tim King [Mon, 1 Feb 2016 19:28:33 +0000 (11:28 -0800)]
Generalizing the implementation of lib/clock_gettime.c so that it can always be compiled.

8 years agoFixing a potentially malformed template expansion when Dump() is disabled.
Tim King [Mon, 1 Feb 2016 19:25:29 +0000 (11:25 -0800)]
Fixing a potentially malformed template expansion when Dump() is disabled.

8 years agoFixing a memory leak in bv_subtheory_algebraic.cpp. Also formatting the file.
Tim King [Mon, 1 Feb 2016 19:22:12 +0000 (11:22 -0800)]
Fixing a memory leak in bv_subtheory_algebraic.cpp. Also formatting the file.

8 years agoAdding an virtual destructor to OstreamUpdate.
Tim King [Mon, 1 Feb 2016 19:12:10 +0000 (11:12 -0800)]
Adding an virtual destructor to OstreamUpdate.

8 years agoMaking the ManagedOstream::defaultSource() a const function.
Tim King [Mon, 1 Feb 2016 19:10:51 +0000 (11:10 -0800)]
Making the ManagedOstream::defaultSource() a const function.

8 years agoAdding a destructor to ProofOutputChannel.
Tim King [Mon, 1 Feb 2016 19:09:09 +0000 (11:09 -0800)]
Adding a destructor to ProofOutputChannel.

8 years agoFixing white spaces in sat_proof.h.
Tim King [Mon, 1 Feb 2016 19:07:41 +0000 (11:07 -0800)]
Fixing white spaces in sat_proof.h.

8 years agoMaking the references to std more explicit in didyoumean.cpp.
Tim King [Mon, 1 Feb 2016 18:59:49 +0000 (10:59 -0800)]
Making the references to std more explicit in didyoumean.cpp.

8 years agoFixing a memory leak in array info.
Tim King [Mon, 1 Feb 2016 18:56:55 +0000 (10:56 -0800)]
Fixing a memory leak in array info.

8 years agoDeleting the dead code in proof/sat_proof.cpp.
Tim King [Mon, 1 Feb 2016 18:54:45 +0000 (10:54 -0800)]
Deleting the dead code in proof/sat_proof.cpp.

8 years agoSimplify fmc model construction, add regression. Improve FMF debug assertions.
ajreynol [Mon, 1 Feb 2016 17:18:00 +0000 (11:18 -0600)]
Simplify fmc model construction, add regression. Improve FMF debug assertions.

8 years agoAdding listeners to Options.
Tim King [Thu, 28 Jan 2016 20:35:45 +0000 (12:35 -0800)]
Adding listeners to Options.
- Options
-- Added the new option attribute :notify. One can get a notify() call on the Listener after a the option's value is updated. This is the new preferred way to achieve dynamic dispatch for options.
-- Removed SmtOptionsHandler and pushed its functionality into OptionsHandler and Listeners.
-- Added functions to Options for registering listeners of the notify calls.
-- Changed a number of options to use the new listener infrastructure.
-- Fixed a number of warnings in options.
-- Added the ArgumentExtender class to better capture how arguments are inserted while parsing options and ease memory management. Previously this was the "preemptGetopt" procedure.
-- Moved options/options_handler_interface.{cpp,h} to options/options_handler.{cpp,h}.

- Theories
-- Reimplemented alternative theories to use a datastructure stored on TheoryEngine instead of on Options.

- Ostream Handling:
-- Added new functionality that generalized how ostreams are opened, options/open_stream.h.
-- Simplified the memory management for different ostreams, smt/managed_ostreams.h.
-- Had the SmtEnginePrivate manage the memory for the ostreams set by options.
-- Simplified how the setting of ostreams are updated, smt/update_ostream.h.

- Configuration and Tags:
-- Configuration can now be used during predicates and handlers for options.
-- Moved configuration.{cpp,h,i} and configuration_private.h from util/ into base/.
-- Moved {Debug,Trace}_tags.* from being generated in options/ into base/.

- cvc4_private.h
-- Upgraded #warning's in cvc4_private.h and cvc4_private_library.h to #error's.
-- Added public first-order (non-templatized) member functions for options get and set the value of options outside of libcvc4. Fixed all of the use locations.
-- Made lib/lib/clock_gettime.h a cvc4_private_library.h header.

- Antlr
-- Fixed antlr and cvc4 macro definition conflicts that caused warnings.

- SmtGlobals
-- Refactored replayStream and replayLog out of SmtGlobals.
-- Renamed SmtGlobals to LemmaChannels and moved the implementation into smt_util/lemma_channels.{h,cpp}.

8 years agoMerged bit-vector and uf proof branch.
Liana Hadarean [Wed, 27 Jan 2016 00:04:26 +0000 (16:04 -0800)]
Merged bit-vector and uf proof branch.

8 years agoFix bug in fmc mbqi where modelscomputed for mbqi could involve non-constant values...
ajreynol [Wed, 20 Jan 2016 22:55:02 +0000 (16:55 -0600)]
Fix bug in fmc mbqi where modelscomputed for mbqi could involve non-constant values. Add regression.

8 years agoBug fixes for model construction with codatatypes, add regressions.
ajreynol [Tue, 19 Jan 2016 18:21:50 +0000 (12:21 -0600)]
Bug fixes for model construction with codatatypes, add regressions.

8 years agoBug fix rewriter for fun defs.
ajreynol [Mon, 18 Jan 2016 21:33:22 +0000 (22:33 +0100)]
Bug fix rewriter for fun defs.

8 years agoType enumerators take optional argument indicating fixed cardinalities of uninterpret...
ajreynol [Fri, 15 Jan 2016 22:57:56 +0000 (23:57 +0100)]
Type enumerators take optional argument indicating fixed cardinalities of uninterpreted sorts. Modify TheoryModelBuilder.  Fix bug in fmf-empty-sorts.

8 years agoEnsure model construction for parametric sorts involving uninterpreted sorts respect...
ajreynol [Thu, 14 Jan 2016 23:18:49 +0000 (00:18 +0100)]
Ensure model construction for parametric sorts involving uninterpreted sorts respect cardinality bounds on when finite model finding is enabled.

8 years agoLemma cache datatypes. Do not send true lemma in quantifiers. Minor fix for datatypes...
ajreynol [Wed, 13 Jan 2016 22:08:40 +0000 (23:08 +0100)]
Lemma cache datatypes. Do not send true lemma in quantifiers. Minor fix for datatypes model generation for UFinite datatypes when FMF.

8 years agoAdding a new Listener utility class. Changing the ResourceManager to use Listeners...
Tim King [Sat, 9 Jan 2016 02:19:30 +0000 (18:19 -0800)]
Adding a new Listener utility class. Changing the ResourceManager to use Listeners for reporting hard and soft resource out() events.

8 years agoRemoving StatisticsRegistry's static functions current() and registerStat().
Tim King [Sat, 9 Jan 2016 00:44:57 +0000 (16:44 -0800)]
Removing StatisticsRegistry's static functions current() and registerStat().
- The functionality the get the StatisticsRegistry attached to the SmtEngine was previously through StatisticsRegistry::current(). This is the dominant StatisticsRegistry in the code. (There is another StatisticsRegistry attached to the NodeManager.) Having this be a static function on StatisticsRegistry requires the use of an SmtEngine in the wrong compilation unit.
- Usages of StatisticsRegistry::current() that were visible in prop/{bvminisat,minisat} has been removed. A pointer to the relevant StatisticsRegistry should be passed instead into the constructor.
- The function StatisticsRegistry::current() has been replaced by SmtScope::currentStatisticsRegistry(). SmtScope is in the libcvc4 package, where SmtEngine is available in the compilation unit.
- The function smtStatisticsRegistry() is a synonym for SmtScope::currentStatisticsRegistry() in smt/smt_statistics_registry.h. This header has fewer include dependencies than the one for SmtScope.
- Correspondingly, the static functions StatisticsRegistry::{registerStat, unregisterStat} have been removed. One should instead use smtStatisticsRegistry()->{registerStat,unregisterStat} instead.
- The KEEP_STATISTIC macro has been moved into smt/smt_statistics_registry.h.
- Documents the reason StatisticsRegistry is CVC4_PUBLIC. This lets me remove the warning I added.
- Removing most operators for timespec from statistics_registry.h file. These a bit error prone in clang.
- Most of the really confusing ifdef's in util/statistics_registry.h are gone.

8 years agoDisabling the RESTART command.
Tim King [Fri, 8 Jan 2016 06:39:41 +0000 (01:39 -0500)]
Disabling the RESTART command.

8 years agofix windows builds
Kshitij Bansal [Wed, 6 Jan 2016 21:02:50 +0000 (16:02 -0500)]
fix windows builds

8 years agoFixing a SWIG ordering issue between bitvector and integer.
Tim King [Wed, 6 Jan 2016 20:43:41 +0000 (12:43 -0800)]
Fixing a SWIG ordering issue between bitvector and integer.