diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-02 20:38:23 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-02 20:38:23 +0000 |
| commit | 068107e1d1f705eb9054b4309a26236230687d80 (patch) | |
| tree | 4c422f3efd6a8319abe426c518f9d2feb7ab5a6d | |
| parent | 53176a3d39935bd77f1c057d0b806c380b346e23 (diff) | |
CDMap -> CDHashMap
CDSet -> CDHashSet
37 files changed, 417 insertions, 416 deletions
@@ -52,277 +52,278 @@ <storageModule moduleId="org.eclipse.cdt.core.externalSettings"/> <storageModule moduleId="org.eclipse.cdt.internal.ui.text.commentOwnerProjectMappings"/> <storageModule moduleId="org.eclipse.cdt.core.language.mapping"/> - <storageModule moduleId="scannerConfiguration"> - <autodiscovery enabled="true" problemReportingEnabled="true" selectedProfileId=""/> - <profile id="org.eclipse.cdt.make.core.GCCStandardMakePerProjectProfile"> - <buildOutputProvider> - <openAction enabled="true" filePath=""/> - <parser enabled="true"/> - </buildOutputProvider> - <scannerInfoProvider id="specsFile"> - <runAction arguments="-E -P -v -dD ${plugin_state_location}/${specs_file}" command="gcc" useDefault="true"/> - <parser enabled="true"/> - </scannerInfoProvider> - </profile> - <profile id="org.eclipse.cdt.make.core.GCCStandardMakePerFileProfile"> - <buildOutputProvider> - <openAction enabled="true" filePath=""/> - <parser enabled="true"/> - </buildOutputProvider> - <scannerInfoProvider id="makefileGenerator"> - <runAction arguments="-f ${project_name}_scd.mk" command="make" useDefault="true"/> - <parser enabled="true"/> - </scannerInfoProvider> - </profile> - <profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfile"> - <buildOutputProvider> - <openAction enabled="true" filePath=""/> - <parser enabled="true"/> - </buildOutputProvider> - <scannerInfoProvider id="specsFile"> - <runAction arguments="-E -P -v -dD ${plugin_state_location}/${specs_file}" command="gcc" useDefault="true"/> - <parser enabled="true"/> - </scannerInfoProvider> - </profile> - <profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfileCPP"> - <buildOutputProvider> - <openAction enabled="true" filePath=""/> - <parser enabled="true"/> - </buildOutputProvider> - <scannerInfoProvider id="specsFile"> - <runAction arguments="-E -P -v -dD ${plugin_state_location}/specs.cpp" command="g++" useDefault="true"/> - <parser enabled="true"/> - </scannerInfoProvider> - </profile> - <profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfileC"> - <buildOutputProvider> - <openAction enabled="true" filePath=""/> - <parser enabled="true"/> - </buildOutputProvider> - <scannerInfoProvider id="specsFile"> - <runAction arguments="-E -P -v -dD ${plugin_state_location}/specs.c" command="gcc" useDefault="true"/> - <parser enabled="true"/> - </scannerInfoProvider> - </profile> - <profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfile"> - <buildOutputProvider> - <openAction enabled="true" filePath=""/> - <parser enabled="true"/> - </buildOutputProvider> - <scannerInfoProvider id="specsFile"> - <runAction arguments="-c 'gcc -E -P -v -dD "${plugin_state_location}/${specs_file}"'" command="sh" useDefault="true"/> - <parser enabled="true"/> - </scannerInfoProvider> - </profile> - <profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfileCPP"> - <buildOutputProvider> - <openAction enabled="true" filePath=""/> - <parser enabled="true"/> - </buildOutputProvider> - <scannerInfoProvider id="specsFile"> - <runAction arguments="-c 'g++ -E -P -v -dD "${plugin_state_location}/specs.cpp"'" command="sh" useDefault="true"/> - <parser enabled="true"/> - </scannerInfoProvider> - </profile> - <profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfileC"> - <buildOutputProvider> - <openAction enabled="true" filePath=""/> - <parser enabled="true"/> - </buildOutputProvider> - <scannerInfoProvider id="specsFile"> - <runAction arguments="-c 'gcc -E -P -v -dD "${plugin_state_location}/specs.c"'" command="sh" useDefault="true"/> - <parser enabled="true"/> - </scannerInfoProvider> - </profile> - <scannerConfigBuildInfo instanceId="cdt.managedbuild.toolchain.gnu.base.1461790692;cdt.managedbuild.toolchain.gnu.base.1461790692.1059214216;cdt.managedbuild.tool.gnu.cpp.compiler.base.1803857875;cdt.managedbuild.tool.gnu.cpp.compiler.input.1333398893"> - <autodiscovery enabled="true" problemReportingEnabled="false" selectedProfileId="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfileCPP"/> - <profile id="org.eclipse.cdt.make.core.GCCStandardMakePerProjectProfile"> - <buildOutputProvider> - <openAction enabled="true" filePath=""/> - <parser enabled="true"/> - </buildOutputProvider> - <scannerInfoProvider id="specsFile"> - <runAction arguments="-E -P -v -dD ${plugin_state_location}/${specs_file}" command="gcc" useDefault="true"/> - <parser enabled="true"/> - </scannerInfoProvider> - </profile> - <profile id="org.eclipse.cdt.make.core.GCCStandardMakePerFileProfile"> - <buildOutputProvider> - <openAction enabled="true" filePath=""/> - <parser enabled="true"/> - </buildOutputProvider> - <scannerInfoProvider id="makefileGenerator"> - <runAction arguments="-f ${project_name}_scd.mk" command="make" useDefault="true"/> - <parser enabled="true"/> - </scannerInfoProvider> - </profile> - <profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfile"> - <buildOutputProvider> - <openAction enabled="true" filePath=""/> - <parser enabled="true"/> - </buildOutputProvider> - <scannerInfoProvider id="specsFile"> - <runAction arguments="-E -P -v -dD ${plugin_state_location}/${specs_file}" command="gcc" useDefault="true"/> - <parser enabled="true"/> - </scannerInfoProvider> - </profile> - <profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfileCPP"> - <buildOutputProvider> - <openAction enabled="true" filePath=""/> - <parser enabled="true"/> - </buildOutputProvider> - <scannerInfoProvider id="specsFile"> - <runAction arguments="-E -P -v -dD ${plugin_state_location}/specs.cpp" command="g++" useDefault="true"/> - <parser enabled="true"/> - </scannerInfoProvider> - </profile> - <profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfileC"> - <buildOutputProvider> - <openAction enabled="true" filePath=""/> - <parser enabled="true"/> - </buildOutputProvider> - <scannerInfoProvider id="specsFile"> - <runAction arguments="-E -P -v -dD ${plugin_state_location}/specs.c" command="gcc" useDefault="true"/> - <parser enabled="true"/> - </scannerInfoProvider> - </profile> - <profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfile"> - <buildOutputProvider> - <openAction enabled="true" filePath=""/> - <parser enabled="true"/> - </buildOutputProvider> - <scannerInfoProvider id="specsFile"> - <runAction arguments="-c 'gcc -E -P -v -dD "${plugin_state_location}/${specs_file}"'" command="sh" useDefault="true"/> - <parser enabled="true"/> - </scannerInfoProvider> - </profile> - <profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfileCPP"> - <buildOutputProvider> - <openAction enabled="true" filePath=""/> - <parser enabled="true"/> - </buildOutputProvider> - <scannerInfoProvider id="specsFile"> - <runAction arguments="-c 'g++ -E -P -v -dD "${plugin_state_location}/specs.cpp"'" command="sh" useDefault="true"/> - <parser enabled="true"/> - </scannerInfoProvider> - </profile> - <profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfileC"> - <buildOutputProvider> - <openAction enabled="true" filePath=""/> - <parser enabled="true"/> - </buildOutputProvider> - <scannerInfoProvider id="specsFile"> - <runAction arguments="-c 'gcc -E -P -v -dD "${plugin_state_location}/specs.c"'" command="sh" useDefault="true"/> - <parser enabled="true"/> - </scannerInfoProvider> - </profile> - </scannerConfigBuildInfo> - <scannerConfigBuildInfo instanceId="cdt.managedbuild.toolchain.gnu.base.1461790692;cdt.managedbuild.toolchain.gnu.base.1461790692.1059214216;cdt.managedbuild.tool.gnu.c.compiler.base.1860041504;cdt.managedbuild.tool.gnu.c.compiler.input.814325769"> - <autodiscovery enabled="true" problemReportingEnabled="false" selectedProfileId="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfileC"/> - <profile id="org.eclipse.cdt.make.core.GCCStandardMakePerProjectProfile"> - <buildOutputProvider> - <openAction enabled="true" filePath=""/> - <parser enabled="true"/> - </buildOutputProvider> - <scannerInfoProvider id="specsFile"> - <runAction arguments="-E -P -v -dD ${plugin_state_location}/${specs_file}" command="gcc" useDefault="true"/> - <parser enabled="true"/> - </scannerInfoProvider> - </profile> - <profile id="org.eclipse.cdt.make.core.GCCStandardMakePerFileProfile"> - <buildOutputProvider> - <openAction enabled="true" filePath=""/> - <parser enabled="true"/> - </buildOutputProvider> - <scannerInfoProvider id="makefileGenerator"> - <runAction arguments="-f ${project_name}_scd.mk" command="make" useDefault="true"/> - <parser enabled="true"/> - </scannerInfoProvider> - </profile> - <profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfile"> - <buildOutputProvider> - <openAction enabled="true" filePath=""/> - <parser enabled="true"/> - </buildOutputProvider> - <scannerInfoProvider id="specsFile"> - <runAction arguments="-E -P -v -dD ${plugin_state_location}/${specs_file}" command="gcc" useDefault="true"/> - <parser enabled="true"/> - </scannerInfoProvider> - </profile> - <profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfileCPP"> - <buildOutputProvider> - <openAction enabled="true" filePath=""/> - <parser enabled="true"/> - </buildOutputProvider> - <scannerInfoProvider id="specsFile"> - <runAction arguments="-E -P -v -dD ${plugin_state_location}/specs.cpp" command="g++" useDefault="true"/> - <parser enabled="true"/> - </scannerInfoProvider> - </profile> - <profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfileC"> - <buildOutputProvider> - <openAction enabled="true" filePath=""/> - <parser enabled="true"/> - </buildOutputProvider> - <scannerInfoProvider id="specsFile"> - <runAction arguments="-E -P -v -dD ${plugin_state_location}/specs.c" command="gcc" useDefault="true"/> - <parser enabled="true"/> - </scannerInfoProvider> - </profile> - <profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfile"> - <buildOutputProvider> - <openAction enabled="true" filePath=""/> - <parser enabled="true"/> - </buildOutputProvider> - <scannerInfoProvider id="specsFile"> - <runAction arguments="-c 'gcc -E -P -v -dD "${plugin_state_location}/${specs_file}"'" command="sh" useDefault="true"/> - <parser enabled="true"/> - </scannerInfoProvider> - </profile> - <profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfileCPP"> - <buildOutputProvider> - <openAction enabled="true" filePath=""/> - <parser enabled="true"/> - </buildOutputProvider> - <scannerInfoProvider id="specsFile"> - <runAction arguments="-c 'g++ -E -P -v -dD "${plugin_state_location}/specs.cpp"'" command="sh" useDefault="true"/> - <parser enabled="true"/> - </scannerInfoProvider> - </profile> - <profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfileC"> - <buildOutputProvider> - <openAction enabled="true" filePath=""/> - <parser enabled="true"/> - </buildOutputProvider> - <scannerInfoProvider id="specsFile"> - <runAction arguments="-c 'gcc -E -P -v -dD "${plugin_state_location}/specs.c"'" command="sh" useDefault="true"/> - <parser enabled="true"/> - </scannerInfoProvider> - </profile> - </scannerConfigBuildInfo> - </storageModule> - <storageModule moduleId="org.eclipse.cdt.make.core.buildtargets"> - <buildTargets> - <target name="check" path="" targetID="org.eclipse.cdt.build.MakeTargetBuilder"> - <buildCommand>make</buildCommand> - <buildTarget>check</buildTarget> - <stopOnError>true</stopOnError> - <useDefaultCommand>true</useDefaultCommand> - <runAllBuilders>true</runAllBuilders> - </target> - <target name="uf" path="src/theory/uf" targetID="org.eclipse.cdt.build.MakeTargetBuilder"> - <buildCommand>make</buildCommand> - <buildArguments>-j2</buildArguments> - <buildTarget/> - <stopOnError>true</stopOnError> - <useDefaultCommand>true</useDefaultCommand> - <runAllBuilders>true</runAllBuilders> - </target> - </buildTargets> - </storageModule> </cconfiguration> </storageModule> <storageModule moduleId="cdtBuildSystem" version="4.0.0"> <project id="cvc4.null.1129006228" name="cvc4"/> </storageModule> + <storageModule moduleId="refreshScope"/> + <storageModule moduleId="scannerConfiguration"> + <autodiscovery enabled="true" problemReportingEnabled="true" selectedProfileId=""/> + <profile id="org.eclipse.cdt.make.core.GCCStandardMakePerProjectProfile"> + <buildOutputProvider> + <openAction enabled="true" filePath=""/> + <parser enabled="true"/> + </buildOutputProvider> + <scannerInfoProvider id="specsFile"> + <runAction arguments="-E -P -v -dD ${plugin_state_location}/${specs_file}" command="gcc" useDefault="true"/> + <parser enabled="true"/> + </scannerInfoProvider> + </profile> + <profile id="org.eclipse.cdt.make.core.GCCStandardMakePerFileProfile"> + <buildOutputProvider> + <openAction enabled="true" filePath=""/> + <parser enabled="true"/> + </buildOutputProvider> + <scannerInfoProvider id="makefileGenerator"> + <runAction arguments="-f ${project_name}_scd.mk" command="make" useDefault="true"/> + <parser enabled="true"/> + </scannerInfoProvider> + </profile> + <profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfile"> + <buildOutputProvider> + <openAction enabled="true" filePath=""/> + <parser enabled="true"/> + </buildOutputProvider> + <scannerInfoProvider id="specsFile"> + <runAction arguments="-E -P -v -dD ${plugin_state_location}/${specs_file}" command="gcc" useDefault="true"/> + <parser enabled="true"/> + </scannerInfoProvider> + </profile> + <profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfileCPP"> + <buildOutputProvider> + <openAction enabled="true" filePath=""/> + <parser enabled="true"/> + </buildOutputProvider> + <scannerInfoProvider id="specsFile"> + <runAction arguments="-E -P -v -dD ${plugin_state_location}/specs.cpp" command="g++" useDefault="true"/> + <parser enabled="true"/> + </scannerInfoProvider> + </profile> + <profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfileC"> + <buildOutputProvider> + <openAction enabled="true" filePath=""/> + <parser enabled="true"/> + </buildOutputProvider> + <scannerInfoProvider id="specsFile"> + <runAction arguments="-E -P -v -dD ${plugin_state_location}/specs.c" command="gcc" useDefault="true"/> + <parser enabled="true"/> + </scannerInfoProvider> + </profile> + <profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfile"> + <buildOutputProvider> + <openAction enabled="true" filePath=""/> + <parser enabled="true"/> + </buildOutputProvider> + <scannerInfoProvider id="specsFile"> + <runAction arguments="-c 'gcc -E -P -v -dD "${plugin_state_location}/${specs_file}"'" command="sh" useDefault="true"/> + <parser enabled="true"/> + </scannerInfoProvider> + </profile> + <profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfileCPP"> + <buildOutputProvider> + <openAction enabled="true" filePath=""/> + <parser enabled="true"/> + </buildOutputProvider> + <scannerInfoProvider id="specsFile"> + <runAction arguments="-c 'g++ -E -P -v -dD "${plugin_state_location}/specs.cpp"'" command="sh" useDefault="true"/> + <parser enabled="true"/> + </scannerInfoProvider> + </profile> + <profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfileC"> + <buildOutputProvider> + <openAction enabled="true" filePath=""/> + <parser enabled="true"/> + </buildOutputProvider> + <scannerInfoProvider id="specsFile"> + <runAction arguments="-c 'gcc -E -P -v -dD "${plugin_state_location}/specs.c"'" command="sh" useDefault="true"/> + <parser enabled="true"/> + </scannerInfoProvider> + </profile> + <scannerConfigBuildInfo instanceId="cdt.managedbuild.toolchain.gnu.base.1461790692;cdt.managedbuild.toolchain.gnu.base.1461790692.1059214216;cdt.managedbuild.tool.gnu.cpp.compiler.base.1803857875;cdt.managedbuild.tool.gnu.cpp.compiler.input.1333398893"> + <autodiscovery enabled="true" problemReportingEnabled="false" selectedProfileId="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfileCPP"/> + <profile id="org.eclipse.cdt.make.core.GCCStandardMakePerProjectProfile"> + <buildOutputProvider> + <openAction enabled="true" filePath=""/> + <parser enabled="true"/> + </buildOutputProvider> + <scannerInfoProvider id="specsFile"> + <runAction arguments="-E -P -v -dD ${plugin_state_location}/${specs_file}" command="gcc" useDefault="true"/> + <parser enabled="true"/> + </scannerInfoProvider> + </profile> + <profile id="org.eclipse.cdt.make.core.GCCStandardMakePerFileProfile"> + <buildOutputProvider> + <openAction enabled="true" filePath=""/> + <parser enabled="true"/> + </buildOutputProvider> + <scannerInfoProvider id="makefileGenerator"> + <runAction arguments="-f ${project_name}_scd.mk" command="make" useDefault="true"/> + <parser enabled="true"/> + </scannerInfoProvider> + </profile> + <profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfile"> + <buildOutputProvider> + <openAction enabled="true" filePath=""/> + <parser enabled="true"/> + </buildOutputProvider> + <scannerInfoProvider id="specsFile"> + <runAction arguments="-E -P -v -dD ${plugin_state_location}/${specs_file}" command="gcc" useDefault="true"/> + <parser enabled="true"/> + </scannerInfoProvider> + </profile> + <profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfileCPP"> + <buildOutputProvider> + <openAction enabled="true" filePath=""/> + <parser enabled="true"/> + </buildOutputProvider> + <scannerInfoProvider id="specsFile"> + <runAction arguments="-E -P -v -dD ${plugin_state_location}/specs.cpp" command="g++" useDefault="true"/> + <parser enabled="true"/> + </scannerInfoProvider> + </profile> + <profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfileC"> + <buildOutputProvider> + <openAction enabled="true" filePath=""/> + <parser enabled="true"/> + </buildOutputProvider> + <scannerInfoProvider id="specsFile"> + <runAction arguments="-E -P -v -dD ${plugin_state_location}/specs.c" command="gcc" useDefault="true"/> + <parser enabled="true"/> + </scannerInfoProvider> + </profile> + <profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfile"> + <buildOutputProvider> + <openAction enabled="true" filePath=""/> + <parser enabled="true"/> + </buildOutputProvider> + <scannerInfoProvider id="specsFile"> + <runAction arguments="-c 'gcc -E -P -v -dD "${plugin_state_location}/${specs_file}"'" command="sh" useDefault="true"/> + <parser enabled="true"/> + </scannerInfoProvider> + </profile> + <profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfileCPP"> + <buildOutputProvider> + <openAction enabled="true" filePath=""/> + <parser enabled="true"/> + </buildOutputProvider> + <scannerInfoProvider id="specsFile"> + <runAction arguments="-c 'g++ -E -P -v -dD "${plugin_state_location}/specs.cpp"'" command="sh" useDefault="true"/> + <parser enabled="true"/> + </scannerInfoProvider> + </profile> + <profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfileC"> + <buildOutputProvider> + <openAction enabled="true" filePath=""/> + <parser enabled="true"/> + </buildOutputProvider> + <scannerInfoProvider id="specsFile"> + <runAction arguments="-c 'gcc -E -P -v -dD "${plugin_state_location}/specs.c"'" command="sh" useDefault="true"/> + <parser enabled="true"/> + </scannerInfoProvider> + </profile> + </scannerConfigBuildInfo> + <scannerConfigBuildInfo instanceId="cdt.managedbuild.toolchain.gnu.base.1461790692;cdt.managedbuild.toolchain.gnu.base.1461790692.1059214216;cdt.managedbuild.tool.gnu.c.compiler.base.1860041504;cdt.managedbuild.tool.gnu.c.compiler.input.814325769"> + <autodiscovery enabled="true" problemReportingEnabled="false" selectedProfileId="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfileC"/> + <profile id="org.eclipse.cdt.make.core.GCCStandardMakePerProjectProfile"> + <buildOutputProvider> + <openAction enabled="true" filePath=""/> + <parser enabled="true"/> + </buildOutputProvider> + <scannerInfoProvider id="specsFile"> + <runAction arguments="-E -P -v -dD ${plugin_state_location}/${specs_file}" command="gcc" useDefault="true"/> + <parser enabled="true"/> + </scannerInfoProvider> + </profile> + <profile id="org.eclipse.cdt.make.core.GCCStandardMakePerFileProfile"> + <buildOutputProvider> + <openAction enabled="true" filePath=""/> + <parser enabled="true"/> + </buildOutputProvider> + <scannerInfoProvider id="makefileGenerator"> + <runAction arguments="-f ${project_name}_scd.mk" command="make" useDefault="true"/> + <parser enabled="true"/> + </scannerInfoProvider> + </profile> + <profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfile"> + <buildOutputProvider> + <openAction enabled="true" filePath=""/> + <parser enabled="true"/> + </buildOutputProvider> + <scannerInfoProvider id="specsFile"> + <runAction arguments="-E -P -v -dD ${plugin_state_location}/${specs_file}" command="gcc" useDefault="true"/> + <parser enabled="true"/> + </scannerInfoProvider> + </profile> + <profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfileCPP"> + <buildOutputProvider> + <openAction enabled="true" filePath=""/> + <parser enabled="true"/> + </buildOutputProvider> + <scannerInfoProvider id="specsFile"> + <runAction arguments="-E -P -v -dD ${plugin_state_location}/specs.cpp" command="g++" useDefault="true"/> + <parser enabled="true"/> + </scannerInfoProvider> + </profile> + <profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfileC"> + <buildOutputProvider> + <openAction enabled="true" filePath=""/> + <parser enabled="true"/> + </buildOutputProvider> + <scannerInfoProvider id="specsFile"> + <runAction arguments="-E -P -v -dD ${plugin_state_location}/specs.c" command="gcc" useDefault="true"/> + <parser enabled="true"/> + </scannerInfoProvider> + </profile> + <profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfile"> + <buildOutputProvider> + <openAction enabled="true" filePath=""/> + <parser enabled="true"/> + </buildOutputProvider> + <scannerInfoProvider id="specsFile"> + <runAction arguments="-c 'gcc -E -P -v -dD "${plugin_state_location}/${specs_file}"'" command="sh" useDefault="true"/> + <parser enabled="true"/> + </scannerInfoProvider> + </profile> + <profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfileCPP"> + <buildOutputProvider> + <openAction enabled="true" filePath=""/> + <parser enabled="true"/> + </buildOutputProvider> + <scannerInfoProvider id="specsFile"> + <runAction arguments="-c 'g++ -E -P -v -dD "${plugin_state_location}/specs.cpp"'" command="sh" useDefault="true"/> + <parser enabled="true"/> + </scannerInfoProvider> + </profile> + <profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfileC"> + <buildOutputProvider> + <openAction enabled="true" filePath=""/> + <parser enabled="true"/> + </buildOutputProvider> + <scannerInfoProvider id="specsFile"> + <runAction arguments="-c 'gcc -E -P -v -dD "${plugin_state_location}/specs.c"'" command="sh" useDefault="true"/> + <parser enabled="true"/> + </scannerInfoProvider> + </profile> + </scannerConfigBuildInfo> + </storageModule> + <storageModule moduleId="org.eclipse.cdt.make.core.buildtargets"> + <buildTargets> + <target name="check" path="" targetID="org.eclipse.cdt.build.MakeTargetBuilder"> + <buildCommand>make</buildCommand> + <buildArguments>-j10</buildArguments> + <buildTarget>check</buildTarget> + <stopOnError>true</stopOnError> + <useDefaultCommand>false</useDefaultCommand> + <runAllBuilders>true</runAllBuilders> + </target> + <target name="uf" path="src/theory/uf" targetID="org.eclipse.cdt.build.MakeTargetBuilder"> + <buildCommand>make</buildCommand> + <buildArguments>-j2</buildArguments> + <stopOnError>true</stopOnError> + <useDefaultCommand>true</useDefaultCommand> + <runAllBuilders>true</runAllBuilders> + </target> + </buildTargets> + </storageModule> </cproject> diff --git a/src/context/Makefile.am b/src/context/Makefile.am index e40eac099..23607373a 100644 --- a/src/context/Makefile.am +++ b/src/context/Makefile.am @@ -16,10 +16,10 @@ libcontext_la_SOURCES = \ cdlist_forward.h \ cdqueue.h \ cdtrail_queue.h \ - cdmap.h \ - cdmap_forward.h \ - cdset.h \ - cdset_forward.h \ + cdhashmap.h \ + cdhashmap_forward.h \ + cdhashset.h \ + cdhashset_forward.h \ cdcirclist.h \ cdcirclist_forward.h \ cdvector.h \ diff --git a/src/context/cdmap.h b/src/context/cdhashmap.h index 2a5365082..de21515c7 100644 --- a/src/context/cdmap.h +++ b/src/context/cdhashmap.h @@ -24,53 +24,53 @@ ** CDMap<> is something of a work in progress at present (26 May ** 2010), due to some recent discoveries of problems with its ** internal state. Here are some notes on the internal use of - ** CDOmaps that may be useful in figuring out this mess: + ** CDOhash_maps that may be useful in figuring out this mess: ** ** So you have a CDMap<>. ** - ** You insert some (key,value) pairs. Each allocates a CDOmap<> + ** You insert some (key,value) pairs. Each allocates a CDOhash_map<> ** and goes on a doubly-linked list headed by map.d_first and - ** threaded via cdomap.{d_prev,d_next}. CDOmaps are constructed + ** threaded via CDOhash_map.{d_prev,d_next}. CDOhash_maps are constructed ** with a NULL d_map pointer, but then immediately call ** makeCurrent() and set the d_map pointer back to the map. At ** context level 0, this doesn't lead to anything special. In - ** higher context levels, this stores away a CDOmap with a NULL + ** higher context levels, this stores away a CDOhash_map with a NULL ** map pointer at level 0, and a non-NULL map pointer in the ** current context level. (Remember that for later.) ** ** When a key is associated to a new value in a CDMap, its - ** associated CDOmap calls makeCurrent(), then sets the new - ** value. The save object is also a CDOmap (allocated in context + ** associated CDOhash_map calls makeCurrent(), then sets the new + ** value. The save object is also a CDOhash_map (allocated in context ** memory). ** - ** Now, CDOmaps disappear in a variety of ways. + ** Now, CDOhash_maps disappear in a variety of ways. ** ** First, you might pop beyond a "modification of the value" ** scope level, requiring a re-association of the key to an old - ** value. This is easy. CDOmap::restore() does the work, and + ** value. This is easy. CDOhash_map::restore() does the work, and ** the context memory of the save object is reclaimed as usual. ** ** Second, you might pop beyond a "insert the key" scope level, ** requiring that the key be completely removed from the map and - ** its CDOmap object memory freed. Here, the CDOmap is restored + ** its CDOhash_map object memory freed. Here, the CDOhash_map is restored ** to a "NULL-map" state (see above), signaling it to remove ** itself from the map completely and put itself on a "trash ** list" for the map. ** - ** Third, you might obliterate() the key. This calls the CDOmap + ** Third, you might obliterate() the key. This calls the CDOhash_map ** destructor, which calls destroy(), which does a successive ** restore() until level 0. If the key was in the map since ** level 0, the restore() won't remove it, so in that case - ** obliterate() removes it from the map and frees the CDOmap's + ** obliterate() removes it from the map and frees the CDOhash_map's ** memory. ** - ** Fourth, you might delete the CDMap (calling CDMap::~CDMap()). + ** Fourth, you might delete the cdhashmap(calling CDMap::~CDMap()). ** This first calls destroy(), as per ContextObj contract, but - ** CDMap doesn't save/restore itself, so that does nothing at the + ** cdhashmapdoesn't save/restore itself, so that does nothing at the ** CDMap-level. Then it empties the trash. Then, for each ** element in the map, it marks it as being "part of a complete ** map destruction", which essentially short-circuits - ** CDOmap::restore() (see CDOmap::restore()), then deallocates + ** CDOhash_map::restore() (see CDOhash_map::restore()), then deallocates ** it. Finally it asserts that the trash is empty (which it ** should be, since restore() was short-circuited). ** @@ -80,8 +80,8 @@ ** ** CDMap::emptyTrash() simply goes through and calls ** ->deleteSelf() on all elements in the trash. - ** ContextObj::deleteSelf() calls the CDOmap destructor, then - ** frees the memory associated to the CDOmap. CDOmap::~CDOmap() + ** ContextObj::deleteSelf() calls the CDOhash_map destructor, then + ** frees the memory associated to the CDOhash_map. CDOhash_map::~CDOhash_map() ** calls destroy(), which restores as much as possible. (Note, ** though, that since objects placed on the trash have already ** restored to the fullest extent possible, it does nothing.) @@ -98,7 +98,7 @@ #include "context/context.h" #include "util/Assert.h" -#include "context/cdmap_forward.h" +#include "context/cdhashmap_forward.h" namespace CVC4 { namespace context { @@ -106,27 +106,27 @@ namespace context { // Auxiliary class: almost the same as CDO (see cdo.h) template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> > -class CDOmap : public ContextObj { - friend class CDMap<Key, Data, HashFcn>; +class CDOhash_map : public ContextObj { + friend class CDHashMap<Key, Data, HashFcn>; Key d_key; Data d_data; - CDMap<Key, Data, HashFcn>* d_map; + CDHashMap<Key, Data, HashFcn>* d_map; - /** never put this cdmap element on the trash */ + /** never put this cdhashmapelement on the trash */ bool d_noTrash; // Doubly-linked list for keeping track of elements in order of insertion - CDOmap* d_prev; - CDOmap* d_next; + CDOhash_map* d_prev; + CDOhash_map* d_next; virtual ContextObj* save(ContextMemoryManager* pCMM) { - return new(pCMM) CDOmap(*this); + return new(pCMM) CDOhash_map(*this); } virtual void restore(ContextObj* data) { if(d_map != NULL) { - CDOmap* p = static_cast<CDOmap*>(data); + CDOhash_map* p = static_cast<CDOhash_map*>(data); if(p->d_map == NULL) { Assert(d_map->d_map.find(d_key) != d_map->d_map.end() && (*d_map->d_map.find(d_key)).second == this); @@ -163,7 +163,7 @@ class CDOmap : public ContextObj { } /** ensure copy ctor is only called by us */ - CDOmap(const CDOmap& other) : + CDOhash_map(const CDOhash_map& other) : ContextObj(other), d_key(other.d_key), d_data(other.d_data), @@ -174,8 +174,8 @@ class CDOmap : public ContextObj { public: - CDOmap(Context* context, - CDMap<Key, Data, HashFcn>* map, + CDOhash_map(Context* context, + CDHashMap<Key, Data, HashFcn>* map, const Key& key, const Data& data, bool atLevelZero = false, @@ -212,7 +212,7 @@ public: } d_map = map; - CDOmap*& first = d_map->d_first; + CDOhash_map*& first = d_map->d_first; if(first == NULL) { first = d_next = d_prev = this; Debug("gc") << "add first-elem " << this << " to map " << d_map << std::endl; @@ -225,7 +225,7 @@ public: } } - ~CDOmap() throw(AssertionException) { + ~CDOhash_map() throw(AssertionException) { destroy(); } @@ -251,14 +251,14 @@ public: return data; } - CDOmap* next() const { + CDOhash_map* next() const { if(d_next == d_map->d_first) { return NULL; } else { return d_next; } } -};/* class CDOmap<> */ +};/* class CDOhash_map<> */ /** @@ -267,12 +267,12 @@ public: * defined for the data class, and operator== for the key class. */ template <class Key, class Data, class HashFcn> -class CDMap : public ContextObj { +class CDHashMap : public ContextObj { - typedef CDOmap<Key, Data, HashFcn> Element; + typedef CDOhash_map<Key, Data, HashFcn> Element; typedef __gnu_cxx::hash_map<Key, Element*, HashFcn> table_type; - friend class CDOmap<Key, Data, HashFcn>; + friend class CDOhash_map<Key, Data, HashFcn>; table_type d_map; @@ -304,7 +304,7 @@ class CDMap : public ContextObj { public: - CDMap(Context* context) : + CDHashMap(Context* context) : ContextObj(context), d_map(), d_first(NULL), @@ -312,14 +312,14 @@ public: d_trash() { } - ~CDMap() throw(AssertionException) { - Debug("gc") << "cdmap " << this + ~CDHashMap() throw(AssertionException) { + Debug("gc") << "cdhashmap" << this << " disappearing, destroying..." << std::endl; destroy(); - Debug("gc") << "cdmap " << this + Debug("gc") << "cdhashmap" << this << " disappearing, done destroying" << std::endl; - Debug("gc") << "cdmap " << this << " gone, emptying trash" << std::endl; + Debug("gc") << "cdhashmap" << this << " gone, emptying trash" << std::endl; emptyTrash(); Debug("gc") << "done emptying trash for " << this << std::endl; @@ -339,7 +339,7 @@ public: } void clear() throw(AssertionException) { - Debug("gc") << "clearing cdmap " << this << ", emptying trash" << std::endl; + Debug("gc") << "clearing cdhashmap" << this << ", emptying trash" << std::endl; emptyTrash(); Debug("gc") << "done emptying trash for " << this << std::endl; @@ -464,11 +464,11 @@ public: if(i != d_map.end()) { Debug("gc") << "key " << k << " obliterated" << std::endl; // We can't call ->deleteSelf() here, because it calls the - // ContextObj destructor, which calls CDOmap::destroy(), which - // restore()'s, which puts the CDOmap on the trash, which causes + // ContextObj destructor, which calls CDOhash_map::destroy(), which + // restore()'s, which puts the CDOhash_map on the trash, which causes // a double-delete. (*i).second->~Element(); - // Writing ...->~CDOmap() in the above is legal (?) but breaks + // Writing ...->~CDOhash_map() in the above is legal (?) but breaks // g++ 4.1, though later versions have no problem. typename table_type::iterator j = d_map.find(k); @@ -575,7 +575,7 @@ public: iterator find(const Key& k) { emptyTrash(); - return const_cast<const CDMap*>(this)->find(k); + return const_cast<const CDHashMap*>(this)->find(k); } };/* class CDMap<> */ diff --git a/src/context/cdmap_forward.h b/src/context/cdhashmap_forward.h index 331d6a93e..f1031fec4 100644 --- a/src/context/cdmap_forward.h +++ b/src/context/cdhashmap_forward.h @@ -35,7 +35,7 @@ namespace __gnu_cxx { namespace CVC4 { namespace context { template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> > - class CDMap; + class CDHashMap; }/* CVC4::context namespace */ }/* CVC4 namespace */ diff --git a/src/context/cdset.h b/src/context/cdhashset.h index 8699d9cf4..777bbc94b 100644 --- a/src/context/cdset.h +++ b/src/context/cdhashset.h @@ -22,16 +22,16 @@ #define __CVC4__CONTEXT__CDSET_H #include "context/context.h" -#include "context/cdset_forward.h" -#include "context/cdmap.h" +#include "context/cdhashset_forward.h" +#include "context/cdhashmap.h" #include "util/Assert.h" namespace CVC4 { namespace context { template <class V, class HashFcn> -class CDSet : protected CDMap<V, V, HashFcn> { - typedef CDMap<V, V, HashFcn> super; +class CDHashSet : protected CDHashMap<V, V, HashFcn> { + typedef CDHashMap<V, V, HashFcn> super; public: @@ -52,7 +52,7 @@ public: AlwaysAssert(false, "It is not allowed to delete a ContextObj this way!"); } - CDSet(Context* context) : + CDHashSet(Context* context) : super(context) { } diff --git a/src/context/cdset_forward.h b/src/context/cdhashset_forward.h index 2339552a6..dc7da22d2 100644 --- a/src/context/cdset_forward.h +++ b/src/context/cdhashset_forward.h @@ -35,7 +35,7 @@ namespace __gnu_cxx { namespace CVC4 { namespace context { template <class V, class HashFcn = __gnu_cxx::hash<V> > - class CDSet; + class CDHashSet; }/* CVC4::context namespace */ }/* CVC4 namespace */ diff --git a/src/context/context.h b/src/context/context.h index 4e0832882..f0dbff72b 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -496,7 +496,7 @@ protected: * class-facing interface. This is a "forced" makeCurrent(), useful * for ContextObjs allocated in CMM that need a special "bottom" * case when they disappear out of existence (kind of a destructor). - * See CDOmap (in cdmap.h) for an example. + * See CDOhash_map (in cdhashmap.h) for an example. */ inline void makeSaveRestorePoint() throw(AssertionException); diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h index b359b1666..70535cf1c 100644 --- a/src/expr/attribute_internals.h +++ b/src/expr/attribute_internals.h @@ -27,7 +27,7 @@ #include <ext/hash_map> -#include "context/cdmap.h" +#include "context/cdhashmap.h" namespace CVC4 { namespace expr { @@ -365,12 +365,12 @@ public: */ template <class value_type> class CDAttrHash : - public context::CDMap<std::pair<uint64_t, NodeValue*>, + public context::CDHashMap<std::pair<uint64_t, NodeValue*>, value_type, AttrHashStrategy> { public: CDAttrHash(context::Context* ctxt) : - context::CDMap<std::pair<uint64_t, NodeValue*>, + context::CDHashMap<std::pair<uint64_t, NodeValue*>, value_type, AttrHashStrategy>(ctxt) { } @@ -382,12 +382,12 @@ public: */ template <> class CDAttrHash<bool> : - protected context::CDMap<NodeValue*, + protected context::CDHashMap<NodeValue*, uint64_t, AttrHashBoolStrategy> { /** A "super" type, like in Java, for easy reference below. */ - typedef context::CDMap<NodeValue*, uint64_t, AttrHashBoolStrategy> super; + typedef context::CDHashMap<NodeValue*, uint64_t, AttrHashBoolStrategy> super; /** * BitAccessor allows us to return a bit "by reference." Of course, diff --git a/src/expr/declaration_scope.cpp b/src/expr/declaration_scope.cpp index 37c709b6a..22187ad06 100644 --- a/src/expr/declaration_scope.cpp +++ b/src/expr/declaration_scope.cpp @@ -22,8 +22,8 @@ #include "expr/expr.h" #include "expr/type.h" #include "expr/expr_manager_scope.h" -#include "context/cdmap.h" -#include "context/cdset.h" +#include "context/cdhashmap.h" +#include "context/cdhashset.h" #include "context/context.h" #include <string> @@ -37,9 +37,9 @@ namespace CVC4 { DeclarationScope::DeclarationScope() : d_context(new Context), - d_exprMap(new(true) CDMap<std::string, Expr, StringHashFunction>(d_context)), - d_typeMap(new(true) CDMap<std::string, pair<vector<Type>, Type>, StringHashFunction>(d_context)), - d_functions(new(true) CDSet<Expr, ExprHashFunction>(d_context)) { + d_exprMap(new(true) CDHashMap<std::string, Expr, StringHashFunction>(d_context)), + d_typeMap(new(true) CDHashMap<std::string, pair<vector<Type>, Type>, StringHashFunction>(d_context)), + d_functions(new(true) CDHashSet<Expr, ExprHashFunction>(d_context)) { } DeclarationScope::~DeclarationScope() { @@ -67,7 +67,7 @@ bool DeclarationScope::isBound(const std::string& name) const throw() { } bool DeclarationScope::isBoundDefinedFunction(const std::string& name) const throw() { - CDMap<std::string, Expr, StringHashFunction>::iterator found = + CDHashMap<std::string, Expr, StringHashFunction>::iterator found = d_exprMap->find(name); return found != d_exprMap->end() && d_functions->contains((*found).second); } diff --git a/src/expr/declaration_scope.h b/src/expr/declaration_scope.h index 4bce5e1be..27533cca8 100644 --- a/src/expr/declaration_scope.h +++ b/src/expr/declaration_scope.h @@ -28,8 +28,8 @@ #include "expr/expr.h" #include "util/hash.h" -#include "context/cdset_forward.h" -#include "context/cdmap_forward.h" +#include "context/cdhashset_forward.h" +#include "context/cdhashmap_forward.h" namespace CVC4 { @@ -52,13 +52,13 @@ class CVC4_PUBLIC DeclarationScope { context::Context* d_context; /** A map for expressions. */ - context::CDMap<std::string, Expr, StringHashFunction> *d_exprMap; + context::CDHashMap<std::string, Expr, StringHashFunction> *d_exprMap; /** A map for types. */ - context::CDMap<std::string, std::pair<std::vector<Type>, Type>, StringHashFunction> *d_typeMap; + context::CDHashMap<std::string, std::pair<std::vector<Type>, Type>, StringHashFunction> *d_typeMap; /** A set of defined functions. */ - context::CDSet<Expr, ExprHashFunction> *d_functions; + context::CDHashSet<Expr, ExprHashFunction> *d_functions; public: /** Create a declaration scope. */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3c320b814..8b5a93fa9 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -25,7 +25,7 @@ #include <ext/hash_map> #include "context/cdlist.h" -#include "context/cdset.h" +#include "context/cdhashset.h" #include "context/context.h" #include "expr/command.h" #include "expr/expr.h" @@ -124,7 +124,7 @@ class SmtEnginePrivate { theory::SubstitutionMap d_topLevelSubstitutions; /** - * The last substition that the SAT layer was told about. + * The last substitution that the SAT layer was told about. * In incremental settings, substitutions cannot be performed * "backward," only forward. So SAT needs to be told of all * substitutions that are going to be done. This iterator diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 84d6d1a73..5149ed2e9 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -24,8 +24,8 @@ #include <vector> #include "context/cdlist_forward.h" -#include "context/cdmap_forward.h" -#include "context/cdset_forward.h" +#include "context/cdhashmap_forward.h" +#include "context/cdhashset_forward.h" #include "expr/expr.h" #include "expr/expr_manager.h" #include "util/proof.h" @@ -89,12 +89,12 @@ namespace smt { class CVC4_PUBLIC SmtEngine { /** The type of our internal map of defined functions */ - typedef context::CDMap<Node, smt::DefinedFunction, NodeHashFunction> + typedef context::CDHashMap<Node, smt::DefinedFunction, NodeHashFunction> DefinedFunctionMap; /** The type of our internal assertion list */ typedef context::CDList<Expr> AssertionList; /** The type of our internal assignment set */ - typedef context::CDSet<Node, NodeHashFunction> AssignmentSet; + typedef context::CDHashSet<Node, NodeHashFunction> AssignmentSet; /** Expr manager context */ context::Context* d_context; diff --git a/src/theory/arith/arith_prop_manager.cpp b/src/theory/arith/arith_prop_manager.cpp index 6d2e04de1..4b52133da 100644 --- a/src/theory/arith/arith_prop_manager.cpp +++ b/src/theory/arith/arith_prop_manager.cpp @@ -23,7 +23,7 @@ #include "theory/arith/arith_utilities.h" #include "context/context.h" #include "context/cdlist.h" -#include "context/cdmap.h" +#include "context/cdhashmap.h" #include "context/cdo.h" using namespace CVC4; diff --git a/src/theory/arith/arith_prop_manager.h b/src/theory/arith/arith_prop_manager.h index bf7564593..2bac21437 100644 --- a/src/theory/arith/arith_prop_manager.h +++ b/src/theory/arith/arith_prop_manager.h @@ -29,7 +29,7 @@ #include "theory/arith/delta_rational.h" #include "context/context.h" #include "context/cdlist.h" -#include "context/cdmap.h" +#include "context/cdhashmap.h" #include "context/cdo.h" #include "theory/rewriter.h" #include "util/stats.h" @@ -59,7 +59,7 @@ private: * to its corresponding PropUnit. * This is node is potentially both the consequent or Rewriter::rewrite(consequent). */ - typedef context::CDMap<Node, size_t, NodeHashFunction> ExplainMap; + typedef context::CDHashMap<Node, size_t, NodeHashFunction> ExplainMap; ExplainMap d_explanationMap; size_t getIndex(TNode n) const { diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 07387c977..44b55440e 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -26,7 +26,7 @@ #include "expr/node.h" #include "expr/attribute.h" #include "theory/arith/delta_rational.h" -#include "context/cdset.h" +#include "context/cdhashset.h" #include <vector> #include <stdint.h> #include <limits> @@ -47,9 +47,9 @@ typedef __gnu_cxx::hash_map<ArithVar, Node> ArithVarToNodeMap; //Sets of Nodes typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet; -typedef context::CDSet<Node, NodeHashFunction> CDNodeSet; +typedef context::CDHashSet<Node, NodeHashFunction> CDNodeSet; -typedef context::CDSet<ArithVar> CDArithVarSet; +typedef context::CDHashSet<ArithVar> CDArithVarSet; class ArithVarCallBack { public: diff --git a/src/theory/arith/arithvar_node_map.h b/src/theory/arith/arithvar_node_map.h index df82fde91..1dc8ddf38 100644 --- a/src/theory/arith/arithvar_node_map.h +++ b/src/theory/arith/arithvar_node_map.h @@ -26,7 +26,7 @@ #include "theory/arith/arith_utilities.h" #include "context/context.h" #include "context/cdlist.h" -#include "context/cdmap.h" +#include "context/cdhashmap.h" #include "context/cdo.h" namespace CVC4 { diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index fcac6f10e..bea87fdde 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -1030,8 +1030,8 @@ Node TheoryArith::roundRobinBranch(){ bool TheoryArith::splitDisequalities(){ bool splitSomething = false; - context::CDSet<Node, NodeHashFunction>::iterator it = d_diseq.begin(); - context::CDSet<Node, NodeHashFunction>::iterator it_end = d_diseq.end(); + context::CDHashSet<Node, NodeHashFunction>::iterator it = d_diseq.begin(); + context::CDHashSet<Node, NodeHashFunction>::iterator it_end = d_diseq.end(); for(; it != it_end; ++ it) { TNode eq = (*it)[0]; Assert(eq.getKind() == kind::EQUAL); @@ -1073,8 +1073,8 @@ void TheoryArith::debugPrintAssertions() { Debug("arith::print_assertions") << uConstr << endl; } } - context::CDSet<Node, NodeHashFunction>::iterator it = d_diseq.begin(); - context::CDSet<Node, NodeHashFunction>::iterator it_end = d_diseq.end(); + context::CDHashSet<Node, NodeHashFunction>::iterator it = d_diseq.begin(); + context::CDHashSet<Node, NodeHashFunction>::iterator it_end = d_diseq.end(); for(; it != it_end; ++ it) { Debug("arith::print_assertions") << *it << endl; } diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index f364885c2..e6bdbfba0 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -23,7 +23,7 @@ #include "theory/theory.h" #include "context/context.h" #include "context/cdlist.h" -#include "context/cdset.h" +#include "context/cdhashset.h" #include "expr/node.h" #include "theory/arith/arith_utilities.h" @@ -183,7 +183,7 @@ private: /** * List of all of the inequalities asserted in the current context. */ - context::CDSet<Node, NodeHashFunction> d_diseq; + context::CDHashSet<Node, NodeHashFunction> d_diseq; /** * Manages information about the assignment and upper and lower bounds on diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h index fcc45bbd5..d1c435b48 100644 --- a/src/theory/arrays/array_info.h +++ b/src/theory/arrays/array_info.h @@ -41,7 +41,7 @@ #define __CVC4__THEORY__ARRAYS__ARRAY_INFO_H #include "util/backtrackable.h" #include "context/cdlist.h" -#include "context/cdmap.h" +#include "context/cdhashmap.h" #include "expr/node.h" #include "util/stats.h" #include "util/ntuple.h" diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index d699617e2..fcb6ee382 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -152,8 +152,8 @@ private: typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > CTNodeListAlloc; - typedef context::CDMap<Node, CTNodeListAlloc*, NodeHashFunction> CNodeTNodesMap; - typedef context::CDMap<TNode, List<TNode>*, TNodeHashFunction > EqLists; + typedef context::CDHashMap<Node, CTNodeListAlloc*, NodeHashFunction> CNodeTNodesMap; + typedef context::CDHashMap<TNode, List<TNode>*, TNodeHashFunction > EqLists; typedef __gnu_cxx::hash_map<TNode, CTNodeList*, TNodeHashFunction> NodeTNodesMap; @@ -174,7 +174,7 @@ private: /** List of disequalities needed to construct explanations for propagated * row lemmas */ - context::CDMap<TNode, std::pair<TNode, TNode>, TNodeHashFunction> d_explanations; + context::CDHashMap<TNode, std::pair<TNode, TNode>, TNodeHashFunction> d_explanations; /** * stores the conflicting disequality (still need to call construct @@ -447,9 +447,9 @@ public: void propagate(Effort e) { - Trace("arrays-prop")<<"Propagating \n"; + // Trace("arrays-prop")<<"Propagating \n"; - context::CDList<TNode>::const_iterator it = d_prop_queue.begin(); + // context::CDList<TNode>::const_iterator it = d_prop_queue.begin(); /* for(; it!= d_prop_queue.end(); it++) { TNode eq = *it; diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index 2f9a8f928..78221a617 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -28,8 +28,8 @@ #include "context/context.h" #include "util/hash.h" #include "expr/node.h" -#include "context/cdset.h" -#include "context/cdmap.h" +#include "context/cdhashset.h" +#include "context/cdhashmap.h" #include "context/cdo.h" namespace CVC4 { @@ -113,12 +113,12 @@ private: /** Nodes that have been attached already (computed forward edges for) */ // All the nodes we've visited so far - context::CDSet<TNode, TNodeHashFunction> d_seen; + context::CDHashSet<TNode, TNodeHashFunction> d_seen; /** * Assignment status of each node. */ - typedef context::CDMap<TNode, AssignmentStatus, TNodeHashFunction> AssignmentMap; + typedef context::CDHashMap<TNode, AssignmentStatus, TNodeHashFunction> AssignmentMap; AssignmentMap d_state; /** diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp index 6967bff98..dacd6a538 100644 --- a/src/theory/bv/bitblast_strategies.cpp +++ b/src/theory/bv/bitblast_strategies.cpp @@ -79,7 +79,7 @@ void inline rshift(Bits& bits, unsigned amount) { } void inline lshift(Bits& bits, unsigned amount) { - for (int i = bits.size() - 1; i >= amount ; --i) { + for (int i = (int)bits.size() - 1; i >= (int)amount ; --i) { bits[i] = bits[i-amount]; } for(unsigned i = 0; i < amount; ++i) { diff --git a/src/theory/bv/bv_sat.h b/src/theory/bv/bv_sat.h index ee48dbef4..773491fd0 100644 --- a/src/theory/bv/bv_sat.h +++ b/src/theory/bv/bv_sat.h @@ -30,7 +30,7 @@ #include <ext/hash_map> #include "context/cdo.h" -#include "context/cdset.h" +#include "context/cdhashset.h" #include "context/cdlist.h" #include "theory_bv_utils.h" diff --git a/src/theory/datatypes/explanation_manager.cpp b/src/theory/datatypes/explanation_manager.cpp index 6107e7f2c..be0bf6805 100644 --- a/src/theory/datatypes/explanation_manager.cpp +++ b/src/theory/datatypes/explanation_manager.cpp @@ -47,7 +47,7 @@ void ExplanationManager::process( Node n, NodeBuilder<>& nb, ProofManager* pm ) } }else{ if( !pm->hasExplained( n ) ){ - context::CDMap< Node, Reason, NodeHashFunction >::iterator it = d_drv_map.find( n ); + context::CDHashMap< Node, Reason, NodeHashFunction >::iterator it = d_drv_map.find( n ); Reason r; Node exp; if( it!=d_drv_map.end() ){ diff --git a/src/theory/datatypes/explanation_manager.h b/src/theory/datatypes/explanation_manager.h index 2232d0048..fa0d3f818 100644 --- a/src/theory/datatypes/explanation_manager.h +++ b/src/theory/datatypes/explanation_manager.h @@ -160,7 +160,7 @@ class ExplanationManager : public Explainer { private: /** map from nodes and the reason for them */ - context::CDMap< Node, Reason, NodeHashFunction > d_drv_map; + context::CDHashMap< Node, Reason, NodeHashFunction > d_drv_map; /** has conflict */ context::CDO< bool > d_hasConflict; /** process the reason for node n */ diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 4d429bc54..921df028e 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -40,10 +40,10 @@ namespace datatypes { class TheoryDatatypes : public Theory { private: typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > EqList; - typedef context::CDMap<Node, EqList*, NodeHashFunction> EqLists; + typedef context::CDHashMap<Node, EqList*, NodeHashFunction> EqLists; typedef context::CDList<Node, context::ContextMemoryAllocator<Node> > EqListN; - typedef context::CDMap<Node, EqListN*, NodeHashFunction> EqListsN; - typedef context::CDMap< Node, bool, NodeHashFunction > BoolMap; + typedef context::CDHashMap<Node, EqListN*, NodeHashFunction> EqListsN; + typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; /** for debugging */ context::CDList<Node> d_currAsserts; diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index a5481b807..2efd121a0 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -51,11 +51,11 @@ private: /** Context-dependent size of the d_addedSharedTerms list */ context::CDO<unsigned> d_addedSharedTermsSize; - typedef context::CDMap<std::pair<Node, TNode>, theory::Theory::Set, TNodePairHashFunction> SharedTermsTheoriesMap; + typedef context::CDHashMap<std::pair<Node, TNode>, theory::Theory::Set, TNodePairHashFunction> SharedTermsTheoriesMap; /** A map from atoms and subterms to the theories that use it */ SharedTermsTheoriesMap d_termsToTheories; - typedef context::CDMap<TNode, theory::Theory::Set, TNodeHashFunction> AlreadyNotifiedMap; + typedef context::CDHashMap<TNode, theory::Theory::Set, TNodeHashFunction> AlreadyNotifiedMap; /** Map from term to theories that have already been notified about the shared term */ AlreadyNotifiedMap d_alreadyNotifiedMap; diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h index 1ade4815d..27c1a2b69 100644 --- a/src/theory/substitutions.h +++ b/src/theory/substitutions.h @@ -28,7 +28,7 @@ #include "expr/node.h" #include "context/context.h" #include "context/cdo.h" -#include "context/cdmap.h" +#include "context/cdhashmap.h" #include "util/hash.h" namespace CVC4 { @@ -46,7 +46,7 @@ class SubstitutionMap { public: - typedef context::CDMap<Node, Node, NodeHashFunction> NodeMap; + typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap; typedef NodeMap::iterator iterator; typedef NodeMap::const_iterator const_iterator; diff --git a/src/theory/term_registration_visitor.h b/src/theory/term_registration_visitor.h index edb759157..74b756a03 100644 --- a/src/theory/term_registration_visitor.h +++ b/src/theory/term_registration_visitor.h @@ -36,7 +36,7 @@ class PreRegisterVisitor { /** * Map from nodes to the theories that have already seen them. */ - typedef context::CDMap<TNode, theory::Theory::Set, TNodeHashFunction> TNodeVisitedMap; + typedef context::CDHashMap<TNode, theory::Theory::Set, TNodeHashFunction> TNodeVisitedMap; TNodeVisitedMap d_visited; /** diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 72244a573..4c9309fb6 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -28,7 +28,7 @@ #include "expr/node.h" #include "expr/command.h" #include "prop/prop_engine.h" -#include "context/cdset.h" +#include "context/cdhashset.h" #include "theory/theory.h" #include "theory/substitutions.h" #include "theory/rewriter.h" @@ -121,7 +121,7 @@ class TheoryEngine { * context-dependent set of those theory-propagable literals that * have been propagated. */ - context::CDSet<TNode, TNodeHashFunction> d_hasPropagated; + context::CDHashSet<TNode, TNodeHashFunction> d_hasPropagated; /** * Statistics for a particular theory. @@ -311,7 +311,7 @@ class TheoryEngine { /** * Map from equalities asserted to a theory, to the theory that can explain them. */ - typedef context::CDMap<NodeTheoryPair, NodeTheoryPair, NodeTheoryPairHashFunction> SharedAssertionsMap; + typedef context::CDHashMap<NodeTheoryPair, NodeTheoryPair, NodeTheoryPairHashFunction> SharedAssertionsMap; /** * A map from asserted facts to where they came from (for explanations). diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index ab391e242..cb7674342 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -30,7 +30,7 @@ #include "theory/uf/symmetry_breaker.h" #include "context/cdo.h" -#include "context/cdset.h" +#include "context/cdhashset.h" namespace CVC4 { namespace theory { diff --git a/src/util/congruence_closure.h b/src/util/congruence_closure.h index 4e690ec16..ed1cecd7b 100644 --- a/src/util/congruence_closure.h +++ b/src/util/congruence_closure.h @@ -30,8 +30,8 @@ #include "expr/node.h" #include "context/context_mm.h" #include "context/cdo.h" -#include "context/cdmap.h" -#include "context/cdset.h" +#include "context/cdhashmap.h" +#include "context/cdhashset.h" #include "context/cdlist_context_memory.h" #include "util/exception.h" #include "context/stacking_map.h" @@ -141,15 +141,15 @@ class CongruenceClosure { // typedef all of these so that iterators are easy to define typedef context::StackingMap<Node, Node, NodeHashFunction> RepresentativeMap; typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > ClassList; - typedef context::CDMap<Node, ClassList*, NodeHashFunction> ClassLists; + typedef context::CDHashMap<Node, ClassList*, NodeHashFunction> ClassLists; typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > UseList; - typedef context::CDMap<TNode, UseList*, TNodeHashFunction> UseLists; - typedef context::CDMap<Node, Node, NodeHashFunction> LookupMap; + typedef context::CDHashMap<TNode, UseList*, TNodeHashFunction> UseLists; + typedef context::CDHashMap<Node, Node, NodeHashFunction> LookupMap; typedef __gnu_cxx::hash_map<TNode, Node, TNodeHashFunction> EqMap; - typedef context::CDMap<Node, Node, NodeHashFunction> ProofMap; - typedef context::CDMap<Node, Node, NodeHashFunction> ProofLabel; + typedef context::CDHashMap<Node, Node, NodeHashFunction> ProofMap; + typedef context::CDHashMap<Node, Node, NodeHashFunction> ProofLabel; // Simple, NON-context-dependent pending list, union find and "seen // set" types for constructing explanations and @@ -164,7 +164,7 @@ class CongruenceClosure { LookupMap d_lookup; EqMap d_eqMap; - context::CDSet<TNode, TNodeHashFunction> d_added; + context::CDHashSet<TNode, TNodeHashFunction> d_added; ProofMap d_proof; ProofLabel d_proofLabel; @@ -175,7 +175,7 @@ class CongruenceClosure { * The set of terms we care about (i.e. those that have been given * us with addTerm() and their representatives). */ - typedef context::CDSet<TNode, TNodeHashFunction> CareSet; + typedef context::CDHashSet<TNode, TNodeHashFunction> CareSet; CareSet d_careSet; // === STATISTICS === diff --git a/src/util/trans_closure.cpp b/src/util/trans_closure.cpp index 5d772b576..ba289080c 100644 --- a/src/util/trans_closure.cpp +++ b/src/util/trans_closure.cpp @@ -98,7 +98,7 @@ void TransitiveClosure::debugPrintMatrix() } unsigned TransitiveClosureNode::getId( Node i ){ - context::CDMap< Node, unsigned, NodeHashFunction >::iterator it = nodeMap.find( i ); + context::CDHashMap< Node, unsigned, NodeHashFunction >::iterator it = nodeMap.find( i ); if( it==nodeMap.end() ){ unsigned c = d_counter.get(); nodeMap[i] = c; diff --git a/src/util/trans_closure.h b/src/util/trans_closure.h index a551d4a31..3cb3385dd 100644 --- a/src/util/trans_closure.h +++ b/src/util/trans_closure.h @@ -26,7 +26,7 @@ #include <map> #include "context/cdlist.h" -#include "context/cdmap.h" +#include "context/cdhashmap.h" #include "context/cdo.h" namespace CVC4 { @@ -128,7 +128,7 @@ public: */ class TransitiveClosureNode : public TransitiveClosure{ context::CDO< unsigned > d_counter; - context::CDMap< Node, unsigned, NodeHashFunction > nodeMap; + context::CDHashMap< Node, unsigned, NodeHashFunction > nodeMap; //for debugging context::CDList< std::pair< Node, Node > > currEdges; public: diff --git a/test/unit/context/cdmap_black.h b/test/unit/context/cdmap_black.h index eb2caa98f..0358d1edd 100644 --- a/test/unit/context/cdmap_black.h +++ b/test/unit/context/cdmap_black.h @@ -18,7 +18,7 @@ #include <cxxtest/TestSuite.h> -#include "context/cdmap.h" +#include "context/cdhashmap.h" #include "context/cdlist.h" using namespace std; @@ -43,7 +43,7 @@ public: } void testSimpleSequence() { - CDMap<int, int> map(d_context); + CDHashMap<int, int> map(d_context); TS_ASSERT(map.find(3) == map.end()); TS_ASSERT(map.find(5) == map.end()); @@ -188,7 +188,7 @@ public: // no intervening find() in this one // (under the theory that this could trigger a bug) void testSimpleSequenceFewerFinds() { - CDMap<int, int> map(d_context); + CDHashMap<int, int> map(d_context); map.insert(3, 4); @@ -226,7 +226,7 @@ public: } void testObliterate() { - CDMap<int, int> map(d_context); + CDHashMap<int, int> map(d_context); map.insert(3, 4); @@ -357,7 +357,7 @@ public: } void testObliteratePrimordial() { - CDMap<int, int> map(d_context); + CDHashMap<int, int> map(d_context); map.insert(3, 4); @@ -460,7 +460,7 @@ public: } void testObliterateCurrent() { - CDMap<int, int> map(d_context); + CDHashMap<int, int> map(d_context); map.insert(3, 4); @@ -566,7 +566,7 @@ public: } void testInsertAtContextLevelZero() { - CDMap<int, int> map(d_context); + CDHashMap<int, int> map(d_context); map.insert(3, 4); @@ -739,7 +739,7 @@ public: } void testObliterateInsertedAtContextLevelZero() { - CDMap<int, int> map(d_context); + CDHashMap<int, int> map(d_context); map.insert(3, 4); @@ -933,7 +933,7 @@ public: //Debug.on("gc"); //Debug.on("context"); - CDMap<int, CDList<myint>*, int_hasher> map(d_context); + CDHashMap<int, CDList<myint>*, int_hasher> map(d_context); CDList<myint> *list1, *list2, *list3, *list4; @@ -1026,7 +1026,7 @@ public: d_context->push(); // This re-uses context memory used above. the map.clear() - // triggers an emptyTrash() which fails if the CDOmaps are put + // triggers an emptyTrash() which fails if the CDOhash_maps are put // in the trash. (We use insertDataFromContextMemory() above to // keep them out of the trash.) cout << "allocating\n"; @@ -1059,7 +1059,7 @@ public: void testCmmElementsAtLevel0() { // this was crashing - CDMap<int, int*, int_hasher> map(d_context); + CDHashMap<int, int*, int_hasher> map(d_context); int* a = (int*)d_context->getCMM()->newData(sizeof(int)); map.insertDataFromContextMemory(1, a); } diff --git a/test/unit/context/cdmap_white.h b/test/unit/context/cdmap_white.h index 42f9b8563..db940f3ea 100644 --- a/test/unit/context/cdmap_white.h +++ b/test/unit/context/cdmap_white.h @@ -18,7 +18,7 @@ #include <cxxtest/TestSuite.h> -#include "context/cdmap.h" +#include "context/cdhashmap.h" #include "util/Assert.h" using namespace std; @@ -40,7 +40,7 @@ public: } void testUnreachableSaveAndRestore() { - CDMap<int, int> map(d_context); + CDHashMap<int, int> map(d_context); TS_ASSERT_THROWS_NOTHING(map.makeCurrent()); diff --git a/test/unit/util/congruence_closure_white.h b/test/unit/util/congruence_closure_white.h index 187b7dc08..0c14160f7 100644 --- a/test/unit/util/congruence_closure_white.h +++ b/test/unit/util/congruence_closure_white.h @@ -20,8 +20,8 @@ #include <sstream> #include "context/context.h" -#include "context/cdset.h" -#include "context/cdmap.h" +#include "context/cdhashset.h" +#include "context/cdhashmap.h" #include "expr/node.h" #include "expr/kind.h" #include "expr/node_manager.h" @@ -34,8 +34,8 @@ using namespace std; struct MyOutputChannel { - CDSet<Node, NodeHashFunction> d_notifications; - CDMap<Node, Node, NodeHashFunction> d_equivalences; + CDHashSet<Node, NodeHashFunction> d_notifications; + CDHashMap<Node, Node, NodeHashFunction> d_equivalences; NodeManager* d_nm; MyOutputChannel(Context* ctxt, NodeManager* nm) : @@ -50,7 +50,7 @@ struct MyOutputChannel { } TNode find(TNode n) { - CDMap<Node, Node, NodeHashFunction>::iterator i = d_equivalences.find(n); + CDHashMap<Node, Node, NodeHashFunction>::iterator i = d_equivalences.find(n); if(i == d_equivalences.end()) { return n; } else { |