<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>
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 \
--- /dev/null
+/********************* */
+/*! \file cdmap.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): taking, dejan
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Context-dependent map class.
+ **
+ ** Context-dependent map class. Generic templated class for a map
+ ** which must be saved and restored as contexts are pushed and
+ ** popped. Requires that operator= be defined for the data class,
+ ** and operator== for the key class. For key types that don't have a
+ ** __gnu_cxx::hash<>, you should provide an explicit HashFcn.
+ **
+ ** Internal documentation:
+ **
+ ** 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
+ ** 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 CDOhash_map<>
+ ** and goes on a doubly-linked list headed by map.d_first and
+ ** 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 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 CDOhash_map calls makeCurrent(), then sets the new
+ ** value. The save object is also a CDOhash_map (allocated in context
+ ** memory).
+ **
+ ** 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. 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 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 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 CDOhash_map's
+ ** memory.
+ **
+ ** Fourth, you might delete the cdhashmap(calling CDMap::~CDMap()).
+ ** This first calls destroy(), as per ContextObj contract, but
+ ** 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
+ ** 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).
+ **
+ ** Fifth, you might clear() the CDMap. This does exactly the
+ ** same as CDMap::~CDMap(), except that it doesn't call destroy()
+ ** on itself.
+ **
+ ** CDMap::emptyTrash() simply goes through and calls
+ ** ->deleteSelf() on all elements in the trash.
+ ** 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.)
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__CONTEXT__CDMAP_H
+#define __CVC4__CONTEXT__CDMAP_H
+
+#include <vector>
+#include <iterator>
+#include <ext/hash_map>
+
+#include "context/context.h"
+#include "util/Assert.h"
+#include "context/cdhashmap_forward.h"
+
+namespace CVC4 {
+namespace context {
+
+// Auxiliary class: almost the same as CDO (see cdo.h)
+
+template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
+class CDOhash_map : public ContextObj {
+ friend class CDHashMap<Key, Data, HashFcn>;
+
+ Key d_key;
+ Data d_data;
+ CDHashMap<Key, Data, HashFcn>* d_map;
+
+ /** never put this cdhashmapelement on the trash */
+ bool d_noTrash;
+
+ // Doubly-linked list for keeping track of elements in order of insertion
+ CDOhash_map* d_prev;
+ CDOhash_map* d_next;
+
+ virtual ContextObj* save(ContextMemoryManager* pCMM) {
+ return new(pCMM) CDOhash_map(*this);
+ }
+
+ virtual void restore(ContextObj* data) {
+ if(d_map != NULL) {
+ 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);
+ // no longer in map (popped beyond first level in which it was)
+ d_map->d_map.erase(d_key);
+ // If we call deleteSelf() here, it re-enters restore(). So,
+ // put it on a "trash heap" instead, for later deletion.
+ //
+ // FIXME multithreading
+ if(d_map->d_first == this) {
+ Debug("gc") << "remove first-elem " << this << " from map " << d_map << " with next-elem " << d_next << std::endl;
+ if(d_next == this) {
+ Assert(d_prev == this);
+ d_map->d_first = NULL;
+ } else {
+ d_map->d_first = d_next;
+ }
+ } else {
+ Debug("gc") << "remove nonfirst-elem " << this << " from map " << d_map << std::endl;
+ }
+ d_next->d_prev = d_prev;
+ d_prev->d_next = d_next;
+ if(d_noTrash) {
+ Debug("gc") << "CDMap<> no-trash " << this << std::endl;
+ } else {
+ Debug("gc") << "CDMap<> trash push_back " << this << std::endl;
+ //this->deleteSelf();
+ d_map->d_trash.push_back(this);
+ }
+ } else {
+ d_data = p->d_data;
+ }
+ }
+ }
+
+ /** ensure copy ctor is only called by us */
+ CDOhash_map(const CDOhash_map& other) :
+ ContextObj(other),
+ d_key(other.d_key),
+ d_data(other.d_data),
+ d_map(other.d_map),
+ d_prev(NULL),
+ d_next(NULL) {
+ }
+
+public:
+
+ CDOhash_map(Context* context,
+ CDHashMap<Key, Data, HashFcn>* map,
+ const Key& key,
+ const Data& data,
+ bool atLevelZero = false,
+ bool allocatedInCMM = false) :
+ ContextObj(allocatedInCMM, context),
+ d_key(key),
+ d_map(NULL),
+ d_noTrash(allocatedInCMM) {
+
+ // untested, probably unsafe.
+ Assert(!(atLevelZero && allocatedInCMM));
+
+ if(atLevelZero) {
+ // "Initializing" map insertion: this entry will never be
+ // removed from the map, it's inserted at level 0 as an
+ // "initializing" element. See
+ // CDMap<>::insertAtContextLevelZero().
+ d_data = data;
+ } else {
+ // Normal map insertion: first makeCurrent(), then set the data
+ // and then, later, the map. Order is important; we can't
+ // initialize d_map in the constructor init list above, because
+ // we want the restore of d_map to NULL to signal us to remove
+ // the element from the map.
+
+ if(allocatedInCMM) {
+ // Force a save/restore point, even though the object is
+ // allocated here. This is so that we can detect when the
+ // object falls out of the map (otherwise we wouldn't get it).
+ makeSaveRestorePoint();
+ }
+
+ set(data);
+ }
+ d_map = map;
+
+ 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;
+ } else {
+ Debug("gc") << "add nonfirst-elem " << this << " to map " << d_map << " with first-elem " << first << "[" << first->d_prev << " " << first->d_next << std::endl;
+ d_prev = first->d_prev;
+ d_next = first;
+ d_prev->d_next = this;
+ first->d_prev = this;
+ }
+ }
+
+ ~CDOhash_map() throw(AssertionException) {
+ destroy();
+ }
+
+ void set(const Data& data) {
+ makeCurrent();
+ d_data = data;
+ }
+
+ const Key& getKey() const {
+ return d_key;
+ }
+
+ const Data& get() const {
+ return d_data;
+ }
+
+ operator Data() {
+ return get();
+ }
+
+ const Data& operator=(const Data& data) {
+ set(data);
+ return data;
+ }
+
+ CDOhash_map* next() const {
+ if(d_next == d_map->d_first) {
+ return NULL;
+ } else {
+ return d_next;
+ }
+ }
+};/* class CDOhash_map<> */
+
+
+/**
+ * Generic templated class for a map which must be saved and restored
+ * as contexts are pushed and popped. Requires that operator= be
+ * defined for the data class, and operator== for the key class.
+ */
+template <class Key, class Data, class HashFcn>
+class CDHashMap : public ContextObj {
+
+ typedef CDOhash_map<Key, Data, HashFcn> Element;
+ typedef __gnu_cxx::hash_map<Key, Element*, HashFcn> table_type;
+
+ friend class CDOhash_map<Key, Data, HashFcn>;
+
+ table_type d_map;
+
+ Element* d_first;
+ Context* d_context;
+
+ std::vector<Element*> d_trash;
+
+ // Nothing to save; the elements take care of themselves
+ virtual ContextObj* save(ContextMemoryManager* pCMM) {
+ Unreachable();
+ }
+
+ // Similarly, nothing to restore
+ virtual void restore(ContextObj* data) {
+ Unreachable();
+ }
+
+ void emptyTrash() {
+ //FIXME multithreading
+ for(typename std::vector<Element*>::iterator i = d_trash.begin();
+ i != d_trash.end();
+ ++i) {
+ Debug("gc") << "emptyTrash(): " << *i << std::endl;
+ (*i)->deleteSelf();
+ }
+ d_trash.clear();
+ }
+
+public:
+
+ CDHashMap(Context* context) :
+ ContextObj(context),
+ d_map(),
+ d_first(NULL),
+ d_context(context),
+ d_trash() {
+ }
+
+ ~CDHashMap() throw(AssertionException) {
+ Debug("gc") << "cdhashmap" << this
+ << " disappearing, destroying..." << std::endl;
+ destroy();
+ Debug("gc") << "cdhashmap" << this
+ << " disappearing, done destroying" << std::endl;
+
+ Debug("gc") << "cdhashmap" << this << " gone, emptying trash" << std::endl;
+ emptyTrash();
+ Debug("gc") << "done emptying trash for " << this << std::endl;
+
+ for(typename table_type::iterator i = d_map.begin();
+ i != d_map.end();
+ ++i) {
+ // mark it as being a destruction (short-circuit restore())
+ (*i).second->d_map = NULL;
+ if(!(*i).second->d_noTrash) {
+ (*i).second->deleteSelf();
+ }
+ }
+ d_map.clear();
+ d_first = NULL;
+
+ Assert(d_trash.empty());
+ }
+
+ void clear() throw(AssertionException) {
+ Debug("gc") << "clearing cdhashmap" << this << ", emptying trash" << std::endl;
+ emptyTrash();
+ Debug("gc") << "done emptying trash for " << this << std::endl;
+
+ for(typename table_type::iterator i = d_map.begin();
+ i != d_map.end();
+ ++i) {
+ // mark it as being a destruction (short-circuit restore())
+ (*i).second->d_map = NULL;
+ if(!(*i).second->d_noTrash) {
+ (*i).second->deleteSelf();
+ }
+ }
+ d_map.clear();
+ d_first = NULL;
+
+ Assert(d_trash.empty());
+ }
+
+ // The usual operators of map
+
+ size_t size() const {
+ return d_map.size();
+ }
+
+ bool empty() const {
+ return d_map.empty();
+ }
+
+ size_t count(const Key& k) const {
+ return d_map.count(k);
+ }
+
+ // If a key is not present, a new object is created and inserted
+ Element& operator[](const Key& k) {
+ emptyTrash();
+
+ typename table_type::iterator i = d_map.find(k);
+
+ Element* obj;
+ if(i == d_map.end()) {// create new object
+ obj = new(true) Element(d_context, this, k, Data());
+ d_map[k] = obj;
+ } else {
+ obj = (*i).second;
+ }
+ return *obj;
+ }
+
+ bool insert(const Key& k, const Data& d) {
+ emptyTrash();
+
+ typename table_type::iterator i = d_map.find(k);
+
+ if(i == d_map.end()) {// create new object
+ Element* obj = new(true) Element(d_context, this, k, d);
+ d_map[k] = obj;
+ return true;
+ } else {
+ (*i).second->set(d);
+ return false;
+ }
+ }
+
+ // Use this for pointer data d allocated in context memory at this
+ // level. THIS IS HIGHLY EXPERIMENTAL. It seems to work if ALL
+ // your data objects are allocated from context memory.
+ void insertDataFromContextMemory(const Key& k, const Data& d) {
+ emptyTrash();
+
+ AlwaysAssert(d_map.find(k) == d_map.end());
+
+ Element* obj = new(d_context->getCMM()) Element(d_context, this, k, d,
+ false /* atLevelZero */,
+ true /* allocatedInCMM */);
+
+ d_map[k] = obj;
+ }
+
+ /**
+ * Version of insert() for CDMap<> that inserts data value d at
+ * context level zero. This is a special escape hatch for inserting
+ * "initializing" data into the map. Imagine something happens at a
+ * deep context level L that causes insertion into a map, such that
+ * the object should have an "initializing" value v1 below context
+ * level L, and a "current" value v2 at context level L. Then you
+ * can (assuming key k):
+ *
+ * map.insertAtContextLevelZero(k, v1);
+ * map.insert(k, v2);
+ *
+ * The justification for this "escape hatch" has to do with
+ * variables and assignments in theories (e.g., in arithmetic).
+ * Let's say you introduce a new variable x at some deep decision
+ * level (thanks to lazy registration, or a splitting lemma, or
+ * whatever). x might be mapped to something, but for theory
+ * implementation simplicity shouldn't disappear from the map on
+ * backjump; rather, it can take another (legal) value, or a special
+ * value to indicate it needs to be recomputed.
+ *
+ * It is an error (checked via AlwaysAssert()) to
+ * insertAtContextLevelZero() a key that already is in the map.
+ */
+ void insertAtContextLevelZero(const Key& k, const Data& d) {
+ emptyTrash();
+
+ AlwaysAssert(d_map.find(k) == d_map.end());
+
+ Element* obj = new(true) Element(d_context, this, k, d,
+ true /* atLevelZero */);
+ d_map[k] = obj;
+ }
+
+ // FIXME: no erase(), too much hassle to implement efficiently...
+
+ /**
+ * "Obliterating" is kind of like erasing, except it's not
+ * backtrackable; the key is permanently removed from the map.
+ * (Naturally, it can be re-added as a new element.)
+ */
+ void obliterate(const Key& k) {
+ typename table_type::iterator i = d_map.find(k);
+ 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 CDOhash_map::destroy(), which
+ // restore()'s, which puts the CDOhash_map on the trash, which causes
+ // a double-delete.
+ (*i).second->~Element();
+ // 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);
+ // This if() succeeds for objects inserted when in the
+ // zero-scope: they were never save()'d there, so restore()
+ // never gets a NULL map and so they leak.
+ if(j != d_map.end()) {
+ Element* elt = (*j).second;
+ if(d_first == elt) {
+ if(elt->d_next == elt) {
+ Assert(elt->d_prev == elt);
+ d_first = NULL;
+ } else {
+ d_first = elt->d_next;
+ }
+ } else {
+ elt->d_prev->d_next = elt->d_next;
+ elt->d_next->d_prev = elt->d_prev;
+ }
+ d_map.erase(j);//FIXME multithreading
+ Debug("gc") << "key " << k << " obliterated zero-scope: " << elt << std::endl;
+ // was already destructed, so don't call ->deleteSelf()
+ if(!elt->d_noTrash) {
+ ::operator delete(elt);
+ }
+ }
+ }
+ }
+
+ class iterator {
+ const Element* d_it;
+
+ public:
+
+ iterator(const Element* p) : d_it(p) {}
+ iterator(const iterator& i) : d_it(i.d_it) {}
+
+ // Default constructor
+ iterator() {}
+
+ // (Dis)equality
+ bool operator==(const iterator& i) const {
+ return d_it == i.d_it;
+ }
+ bool operator!=(const iterator& i) const {
+ return d_it != i.d_it;
+ }
+
+ // Dereference operators.
+ std::pair<const Key, const Data> operator*() const {
+ return std::pair<const Key, const Data>(d_it->getKey(), d_it->get());
+ }
+
+ // Prefix increment
+ iterator& operator++() {
+ d_it = d_it->next();
+ return *this;
+ }
+
+ // Postfix increment: requires a Proxy object to hold the
+ // intermediate value for dereferencing
+ class Proxy {
+ const std::pair<const Key, Data>* d_pair;
+
+ public:
+
+ Proxy(const std::pair<const Key, Data>& p) : d_pair(&p) {}
+
+ const std::pair<const Key, Data>& operator*() const {
+ return *d_pair;
+ }
+ };/* class CDMap<>::iterator::Proxy */
+
+ // Actual postfix increment: returns Proxy with the old value.
+ // Now, an expression like *i++ will return the current *i, and
+ // then advance the iterator. However, don't try to use
+ // Proxy for anything else.
+ const Proxy operator++(int) {
+ Proxy e(*(*this));
+ ++(*this);
+ return e;
+ }
+ };/* class CDMap<>::iterator */
+
+ typedef iterator const_iterator;
+
+ iterator begin() const {
+ return iterator(d_first);
+ }
+
+ iterator end() const {
+ return iterator(NULL);
+ }
+
+ iterator find(const Key& k) const {
+ typename table_type::const_iterator i = d_map.find(k);
+
+ if(i == d_map.end()) {
+ return end();
+ } else {
+ return iterator((*i).second);
+ }
+ }
+
+ iterator find(const Key& k) {
+ emptyTrash();
+ return const_cast<const CDHashMap*>(this)->find(k);
+ }
+
+};/* class CDMap<> */
+
+}/* CVC4::context namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__CONTEXT__CDMAP_H */
--- /dev/null
+/********************* */
+/*! \file cdmap_forward.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief This is a forward declaration header to declare the CDMap<>
+ ** template
+ **
+ ** This is a forward declaration header to declare the CDMap<>
+ ** template. It's useful if you want to forward-declare CDMap<>
+ ** without including the full cdmap.h header, for example, in a
+ ** public header context.
+ **
+ ** For CDMap<> in particular, it's difficult to forward-declare it
+ ** yourself, becase it has a default template argument.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__CONTEXT__CDMAP_FORWARD_H
+#define __CVC4__CONTEXT__CDMAP_FORWARD_H
+
+namespace __gnu_cxx {
+ template <class Key> struct hash;
+}/* __gnu_cxx namespace */
+
+namespace CVC4 {
+ namespace context {
+ template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
+ class CDHashMap;
+ }/* CVC4::context namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__CONTEXT__CDMAP_FORWARD_H */
--- /dev/null
+/********************* */
+/*! \file cdset.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Context-dependent set class.
+ **
+ ** Context-dependent set class.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__CONTEXT__CDSET_H
+#define __CVC4__CONTEXT__CDSET_H
+
+#include "context/context.h"
+#include "context/cdhashset_forward.h"
+#include "context/cdhashmap.h"
+#include "util/Assert.h"
+
+namespace CVC4 {
+namespace context {
+
+template <class V, class HashFcn>
+class CDHashSet : protected CDHashMap<V, V, HashFcn> {
+ typedef CDHashMap<V, V, HashFcn> super;
+
+public:
+
+ // ensure these are publicly accessible
+ static void* operator new(size_t size, bool b) {
+ return ContextObj::operator new(size, b);
+ }
+
+ static void operator delete(void* pMem, bool b) {
+ return ContextObj::operator delete(pMem, b);
+ }
+
+ void deleteSelf() {
+ this->ContextObj::deleteSelf();
+ }
+
+ static void operator delete(void* pMem) {
+ AlwaysAssert(false, "It is not allowed to delete a ContextObj this way!");
+ }
+
+ CDHashSet(Context* context) :
+ super(context) {
+ }
+
+ size_t size() const {
+ return super::size();
+ }
+
+ size_t count(const V& v) const {
+ return super::count(v);
+ }
+
+ bool insert(const V& v) {
+ return super::insert(v, v);
+ }
+
+ bool contains(const V& v) {
+ return find(v) != end();
+ }
+
+ // FIXME: no erase(), too much hassle to implement efficiently...
+
+ class iterator {
+ typename super::iterator d_it;
+
+ public:
+
+ iterator(const typename super::iterator& it) : d_it(it) {}
+ iterator(const iterator& it) : d_it(it.d_it) {}
+
+ // Default constructor
+ iterator() {}
+
+ // (Dis)equality
+ bool operator==(const iterator& i) const {
+ return d_it == i.d_it;
+ }
+ bool operator!=(const iterator& i) const {
+ return d_it != i.d_it;
+ }
+
+ // Dereference operators.
+ V operator*() const {
+ return (*d_it).first;
+ }
+
+ // Prefix increment
+ iterator& operator++() {
+ ++d_it;
+ return *this;
+ }
+
+ // Postfix increment: requires a Proxy object to hold the
+ // intermediate value for dereferencing
+ class Proxy {
+ const V& d_val;
+
+ public:
+
+ Proxy(const V& v) : d_val(v) {}
+
+ V operator*() const {
+ return d_val;
+ }
+ };/* class CDSet<>::iterator::Proxy */
+
+ // Actual postfix increment: returns Proxy with the old value.
+ // Now, an expression like *i++ will return the current *i, and
+ // then advance the orderedIterator. However, don't try to use
+ // Proxy for anything else.
+ const Proxy operator++(int) {
+ Proxy e(*(*this));
+ ++(*this);
+ return e;
+ }
+ };/* class CDSet<>::iterator */
+
+ typedef iterator const_iterator;
+
+ const_iterator begin() const {
+ return iterator(super::begin());
+ }
+
+ const_iterator end() const {
+ return iterator(super::end());
+ }
+
+ const_iterator find(const V& v) const {
+ return iterator(super::find(v));
+ }
+
+};/* class CDSet */
+
+}/* CVC4::context namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__CONTEXT__CDSET_H */
--- /dev/null
+/********************* */
+/*! \file cdset_forward.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief This is a forward declaration header to declare the CDSet<>
+ ** template
+ **
+ ** This is a forward declaration header to declare the CDSet<>
+ ** template. It's useful if you want to forward-declare CDSet<>
+ ** without including the full cdset.h header, for example, in a
+ ** public header context.
+ **
+ ** For CDSet<> in particular, it's difficult to forward-declare it
+ ** yourself, becase it has a default template argument.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__CONTEXT__CDSET_FORWARD_H
+#define __CVC4__CONTEXT__CDSET_FORWARD_H
+
+namespace __gnu_cxx {
+ template <class Key> struct hash;
+}/* __gnu_cxx namespace */
+
+namespace CVC4 {
+ namespace context {
+ template <class V, class HashFcn = __gnu_cxx::hash<V> >
+ class CDHashSet;
+ }/* CVC4::context namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__CONTEXT__CDSET_FORWARD_H */
+++ /dev/null
-/********************* */
-/*! \file cdmap.h
- ** \verbatim
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): taking, dejan
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Context-dependent map class.
- **
- ** Context-dependent map class. Generic templated class for a map
- ** which must be saved and restored as contexts are pushed and
- ** popped. Requires that operator= be defined for the data class,
- ** and operator== for the key class. For key types that don't have a
- ** __gnu_cxx::hash<>, you should provide an explicit HashFcn.
- **
- ** Internal documentation:
- **
- ** 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:
- **
- ** So you have a CDMap<>.
- **
- ** You insert some (key,value) pairs. Each allocates a CDOmap<>
- ** and goes on a doubly-linked list headed by map.d_first and
- ** threaded via cdomap.{d_prev,d_next}. CDOmaps 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
- ** 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
- ** memory).
- **
- ** Now, CDOmaps 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
- ** 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
- ** 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
- ** 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
- ** memory.
- **
- ** Fourth, you might delete the CDMap (calling CDMap::~CDMap()).
- ** This first calls destroy(), as per ContextObj contract, but
- ** CDMap doesn'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
- ** it. Finally it asserts that the trash is empty (which it
- ** should be, since restore() was short-circuited).
- **
- ** Fifth, you might clear() the CDMap. This does exactly the
- ** same as CDMap::~CDMap(), except that it doesn't call destroy()
- ** on itself.
- **
- ** 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()
- ** 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.)
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__CONTEXT__CDMAP_H
-#define __CVC4__CONTEXT__CDMAP_H
-
-#include <vector>
-#include <iterator>
-#include <ext/hash_map>
-
-#include "context/context.h"
-#include "util/Assert.h"
-#include "context/cdmap_forward.h"
-
-namespace CVC4 {
-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>;
-
- Key d_key;
- Data d_data;
- CDMap<Key, Data, HashFcn>* d_map;
-
- /** never put this cdmap element on the trash */
- bool d_noTrash;
-
- // Doubly-linked list for keeping track of elements in order of insertion
- CDOmap* d_prev;
- CDOmap* d_next;
-
- virtual ContextObj* save(ContextMemoryManager* pCMM) {
- return new(pCMM) CDOmap(*this);
- }
-
- virtual void restore(ContextObj* data) {
- if(d_map != NULL) {
- CDOmap* p = static_cast<CDOmap*>(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);
- // no longer in map (popped beyond first level in which it was)
- d_map->d_map.erase(d_key);
- // If we call deleteSelf() here, it re-enters restore(). So,
- // put it on a "trash heap" instead, for later deletion.
- //
- // FIXME multithreading
- if(d_map->d_first == this) {
- Debug("gc") << "remove first-elem " << this << " from map " << d_map << " with next-elem " << d_next << std::endl;
- if(d_next == this) {
- Assert(d_prev == this);
- d_map->d_first = NULL;
- } else {
- d_map->d_first = d_next;
- }
- } else {
- Debug("gc") << "remove nonfirst-elem " << this << " from map " << d_map << std::endl;
- }
- d_next->d_prev = d_prev;
- d_prev->d_next = d_next;
- if(d_noTrash) {
- Debug("gc") << "CDMap<> no-trash " << this << std::endl;
- } else {
- Debug("gc") << "CDMap<> trash push_back " << this << std::endl;
- //this->deleteSelf();
- d_map->d_trash.push_back(this);
- }
- } else {
- d_data = p->d_data;
- }
- }
- }
-
- /** ensure copy ctor is only called by us */
- CDOmap(const CDOmap& other) :
- ContextObj(other),
- d_key(other.d_key),
- d_data(other.d_data),
- d_map(other.d_map),
- d_prev(NULL),
- d_next(NULL) {
- }
-
-public:
-
- CDOmap(Context* context,
- CDMap<Key, Data, HashFcn>* map,
- const Key& key,
- const Data& data,
- bool atLevelZero = false,
- bool allocatedInCMM = false) :
- ContextObj(allocatedInCMM, context),
- d_key(key),
- d_map(NULL),
- d_noTrash(allocatedInCMM) {
-
- // untested, probably unsafe.
- Assert(!(atLevelZero && allocatedInCMM));
-
- if(atLevelZero) {
- // "Initializing" map insertion: this entry will never be
- // removed from the map, it's inserted at level 0 as an
- // "initializing" element. See
- // CDMap<>::insertAtContextLevelZero().
- d_data = data;
- } else {
- // Normal map insertion: first makeCurrent(), then set the data
- // and then, later, the map. Order is important; we can't
- // initialize d_map in the constructor init list above, because
- // we want the restore of d_map to NULL to signal us to remove
- // the element from the map.
-
- if(allocatedInCMM) {
- // Force a save/restore point, even though the object is
- // allocated here. This is so that we can detect when the
- // object falls out of the map (otherwise we wouldn't get it).
- makeSaveRestorePoint();
- }
-
- set(data);
- }
- d_map = map;
-
- CDOmap*& 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;
- } else {
- Debug("gc") << "add nonfirst-elem " << this << " to map " << d_map << " with first-elem " << first << "[" << first->d_prev << " " << first->d_next << std::endl;
- d_prev = first->d_prev;
- d_next = first;
- d_prev->d_next = this;
- first->d_prev = this;
- }
- }
-
- ~CDOmap() throw(AssertionException) {
- destroy();
- }
-
- void set(const Data& data) {
- makeCurrent();
- d_data = data;
- }
-
- const Key& getKey() const {
- return d_key;
- }
-
- const Data& get() const {
- return d_data;
- }
-
- operator Data() {
- return get();
- }
-
- const Data& operator=(const Data& data) {
- set(data);
- return data;
- }
-
- CDOmap* next() const {
- if(d_next == d_map->d_first) {
- return NULL;
- } else {
- return d_next;
- }
- }
-};/* class CDOmap<> */
-
-
-/**
- * Generic templated class for a map which must be saved and restored
- * as contexts are pushed and popped. Requires that operator= be
- * defined for the data class, and operator== for the key class.
- */
-template <class Key, class Data, class HashFcn>
-class CDMap : public ContextObj {
-
- typedef CDOmap<Key, Data, HashFcn> Element;
- typedef __gnu_cxx::hash_map<Key, Element*, HashFcn> table_type;
-
- friend class CDOmap<Key, Data, HashFcn>;
-
- table_type d_map;
-
- Element* d_first;
- Context* d_context;
-
- std::vector<Element*> d_trash;
-
- // Nothing to save; the elements take care of themselves
- virtual ContextObj* save(ContextMemoryManager* pCMM) {
- Unreachable();
- }
-
- // Similarly, nothing to restore
- virtual void restore(ContextObj* data) {
- Unreachable();
- }
-
- void emptyTrash() {
- //FIXME multithreading
- for(typename std::vector<Element*>::iterator i = d_trash.begin();
- i != d_trash.end();
- ++i) {
- Debug("gc") << "emptyTrash(): " << *i << std::endl;
- (*i)->deleteSelf();
- }
- d_trash.clear();
- }
-
-public:
-
- CDMap(Context* context) :
- ContextObj(context),
- d_map(),
- d_first(NULL),
- d_context(context),
- d_trash() {
- }
-
- ~CDMap() throw(AssertionException) {
- Debug("gc") << "cdmap " << this
- << " disappearing, destroying..." << std::endl;
- destroy();
- Debug("gc") << "cdmap " << this
- << " disappearing, done destroying" << std::endl;
-
- Debug("gc") << "cdmap " << this << " gone, emptying trash" << std::endl;
- emptyTrash();
- Debug("gc") << "done emptying trash for " << this << std::endl;
-
- for(typename table_type::iterator i = d_map.begin();
- i != d_map.end();
- ++i) {
- // mark it as being a destruction (short-circuit restore())
- (*i).second->d_map = NULL;
- if(!(*i).second->d_noTrash) {
- (*i).second->deleteSelf();
- }
- }
- d_map.clear();
- d_first = NULL;
-
- Assert(d_trash.empty());
- }
-
- void clear() throw(AssertionException) {
- Debug("gc") << "clearing cdmap " << this << ", emptying trash" << std::endl;
- emptyTrash();
- Debug("gc") << "done emptying trash for " << this << std::endl;
-
- for(typename table_type::iterator i = d_map.begin();
- i != d_map.end();
- ++i) {
- // mark it as being a destruction (short-circuit restore())
- (*i).second->d_map = NULL;
- if(!(*i).second->d_noTrash) {
- (*i).second->deleteSelf();
- }
- }
- d_map.clear();
- d_first = NULL;
-
- Assert(d_trash.empty());
- }
-
- // The usual operators of map
-
- size_t size() const {
- return d_map.size();
- }
-
- bool empty() const {
- return d_map.empty();
- }
-
- size_t count(const Key& k) const {
- return d_map.count(k);
- }
-
- // If a key is not present, a new object is created and inserted
- Element& operator[](const Key& k) {
- emptyTrash();
-
- typename table_type::iterator i = d_map.find(k);
-
- Element* obj;
- if(i == d_map.end()) {// create new object
- obj = new(true) Element(d_context, this, k, Data());
- d_map[k] = obj;
- } else {
- obj = (*i).second;
- }
- return *obj;
- }
-
- bool insert(const Key& k, const Data& d) {
- emptyTrash();
-
- typename table_type::iterator i = d_map.find(k);
-
- if(i == d_map.end()) {// create new object
- Element* obj = new(true) Element(d_context, this, k, d);
- d_map[k] = obj;
- return true;
- } else {
- (*i).second->set(d);
- return false;
- }
- }
-
- // Use this for pointer data d allocated in context memory at this
- // level. THIS IS HIGHLY EXPERIMENTAL. It seems to work if ALL
- // your data objects are allocated from context memory.
- void insertDataFromContextMemory(const Key& k, const Data& d) {
- emptyTrash();
-
- AlwaysAssert(d_map.find(k) == d_map.end());
-
- Element* obj = new(d_context->getCMM()) Element(d_context, this, k, d,
- false /* atLevelZero */,
- true /* allocatedInCMM */);
-
- d_map[k] = obj;
- }
-
- /**
- * Version of insert() for CDMap<> that inserts data value d at
- * context level zero. This is a special escape hatch for inserting
- * "initializing" data into the map. Imagine something happens at a
- * deep context level L that causes insertion into a map, such that
- * the object should have an "initializing" value v1 below context
- * level L, and a "current" value v2 at context level L. Then you
- * can (assuming key k):
- *
- * map.insertAtContextLevelZero(k, v1);
- * map.insert(k, v2);
- *
- * The justification for this "escape hatch" has to do with
- * variables and assignments in theories (e.g., in arithmetic).
- * Let's say you introduce a new variable x at some deep decision
- * level (thanks to lazy registration, or a splitting lemma, or
- * whatever). x might be mapped to something, but for theory
- * implementation simplicity shouldn't disappear from the map on
- * backjump; rather, it can take another (legal) value, or a special
- * value to indicate it needs to be recomputed.
- *
- * It is an error (checked via AlwaysAssert()) to
- * insertAtContextLevelZero() a key that already is in the map.
- */
- void insertAtContextLevelZero(const Key& k, const Data& d) {
- emptyTrash();
-
- AlwaysAssert(d_map.find(k) == d_map.end());
-
- Element* obj = new(true) Element(d_context, this, k, d,
- true /* atLevelZero */);
- d_map[k] = obj;
- }
-
- // FIXME: no erase(), too much hassle to implement efficiently...
-
- /**
- * "Obliterating" is kind of like erasing, except it's not
- * backtrackable; the key is permanently removed from the map.
- * (Naturally, it can be re-added as a new element.)
- */
- void obliterate(const Key& k) {
- typename table_type::iterator i = d_map.find(k);
- 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
- // a double-delete.
- (*i).second->~Element();
- // Writing ...->~CDOmap() 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);
- // This if() succeeds for objects inserted when in the
- // zero-scope: they were never save()'d there, so restore()
- // never gets a NULL map and so they leak.
- if(j != d_map.end()) {
- Element* elt = (*j).second;
- if(d_first == elt) {
- if(elt->d_next == elt) {
- Assert(elt->d_prev == elt);
- d_first = NULL;
- } else {
- d_first = elt->d_next;
- }
- } else {
- elt->d_prev->d_next = elt->d_next;
- elt->d_next->d_prev = elt->d_prev;
- }
- d_map.erase(j);//FIXME multithreading
- Debug("gc") << "key " << k << " obliterated zero-scope: " << elt << std::endl;
- // was already destructed, so don't call ->deleteSelf()
- if(!elt->d_noTrash) {
- ::operator delete(elt);
- }
- }
- }
- }
-
- class iterator {
- const Element* d_it;
-
- public:
-
- iterator(const Element* p) : d_it(p) {}
- iterator(const iterator& i) : d_it(i.d_it) {}
-
- // Default constructor
- iterator() {}
-
- // (Dis)equality
- bool operator==(const iterator& i) const {
- return d_it == i.d_it;
- }
- bool operator!=(const iterator& i) const {
- return d_it != i.d_it;
- }
-
- // Dereference operators.
- std::pair<const Key, const Data> operator*() const {
- return std::pair<const Key, const Data>(d_it->getKey(), d_it->get());
- }
-
- // Prefix increment
- iterator& operator++() {
- d_it = d_it->next();
- return *this;
- }
-
- // Postfix increment: requires a Proxy object to hold the
- // intermediate value for dereferencing
- class Proxy {
- const std::pair<const Key, Data>* d_pair;
-
- public:
-
- Proxy(const std::pair<const Key, Data>& p) : d_pair(&p) {}
-
- const std::pair<const Key, Data>& operator*() const {
- return *d_pair;
- }
- };/* class CDMap<>::iterator::Proxy */
-
- // Actual postfix increment: returns Proxy with the old value.
- // Now, an expression like *i++ will return the current *i, and
- // then advance the iterator. However, don't try to use
- // Proxy for anything else.
- const Proxy operator++(int) {
- Proxy e(*(*this));
- ++(*this);
- return e;
- }
- };/* class CDMap<>::iterator */
-
- typedef iterator const_iterator;
-
- iterator begin() const {
- return iterator(d_first);
- }
-
- iterator end() const {
- return iterator(NULL);
- }
-
- iterator find(const Key& k) const {
- typename table_type::const_iterator i = d_map.find(k);
-
- if(i == d_map.end()) {
- return end();
- } else {
- return iterator((*i).second);
- }
- }
-
- iterator find(const Key& k) {
- emptyTrash();
- return const_cast<const CDMap*>(this)->find(k);
- }
-
-};/* class CDMap<> */
-
-}/* CVC4::context namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__CONTEXT__CDMAP_H */
+++ /dev/null
-/********************* */
-/*! \file cdmap_forward.h
- ** \verbatim
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief This is a forward declaration header to declare the CDMap<>
- ** template
- **
- ** This is a forward declaration header to declare the CDMap<>
- ** template. It's useful if you want to forward-declare CDMap<>
- ** without including the full cdmap.h header, for example, in a
- ** public header context.
- **
- ** For CDMap<> in particular, it's difficult to forward-declare it
- ** yourself, becase it has a default template argument.
- **/
-
-#include "cvc4_public.h"
-
-#ifndef __CVC4__CONTEXT__CDMAP_FORWARD_H
-#define __CVC4__CONTEXT__CDMAP_FORWARD_H
-
-namespace __gnu_cxx {
- template <class Key> struct hash;
-}/* __gnu_cxx namespace */
-
-namespace CVC4 {
- namespace context {
- template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
- class CDMap;
- }/* CVC4::context namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__CONTEXT__CDMAP_FORWARD_H */
+++ /dev/null
-/********************* */
-/*! \file cdset.h
- ** \verbatim
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Context-dependent set class.
- **
- ** Context-dependent set class.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__CONTEXT__CDSET_H
-#define __CVC4__CONTEXT__CDSET_H
-
-#include "context/context.h"
-#include "context/cdset_forward.h"
-#include "context/cdmap.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;
-
-public:
-
- // ensure these are publicly accessible
- static void* operator new(size_t size, bool b) {
- return ContextObj::operator new(size, b);
- }
-
- static void operator delete(void* pMem, bool b) {
- return ContextObj::operator delete(pMem, b);
- }
-
- void deleteSelf() {
- this->ContextObj::deleteSelf();
- }
-
- static void operator delete(void* pMem) {
- AlwaysAssert(false, "It is not allowed to delete a ContextObj this way!");
- }
-
- CDSet(Context* context) :
- super(context) {
- }
-
- size_t size() const {
- return super::size();
- }
-
- size_t count(const V& v) const {
- return super::count(v);
- }
-
- bool insert(const V& v) {
- return super::insert(v, v);
- }
-
- bool contains(const V& v) {
- return find(v) != end();
- }
-
- // FIXME: no erase(), too much hassle to implement efficiently...
-
- class iterator {
- typename super::iterator d_it;
-
- public:
-
- iterator(const typename super::iterator& it) : d_it(it) {}
- iterator(const iterator& it) : d_it(it.d_it) {}
-
- // Default constructor
- iterator() {}
-
- // (Dis)equality
- bool operator==(const iterator& i) const {
- return d_it == i.d_it;
- }
- bool operator!=(const iterator& i) const {
- return d_it != i.d_it;
- }
-
- // Dereference operators.
- V operator*() const {
- return (*d_it).first;
- }
-
- // Prefix increment
- iterator& operator++() {
- ++d_it;
- return *this;
- }
-
- // Postfix increment: requires a Proxy object to hold the
- // intermediate value for dereferencing
- class Proxy {
- const V& d_val;
-
- public:
-
- Proxy(const V& v) : d_val(v) {}
-
- V operator*() const {
- return d_val;
- }
- };/* class CDSet<>::iterator::Proxy */
-
- // Actual postfix increment: returns Proxy with the old value.
- // Now, an expression like *i++ will return the current *i, and
- // then advance the orderedIterator. However, don't try to use
- // Proxy for anything else.
- const Proxy operator++(int) {
- Proxy e(*(*this));
- ++(*this);
- return e;
- }
- };/* class CDSet<>::iterator */
-
- typedef iterator const_iterator;
-
- const_iterator begin() const {
- return iterator(super::begin());
- }
-
- const_iterator end() const {
- return iterator(super::end());
- }
-
- const_iterator find(const V& v) const {
- return iterator(super::find(v));
- }
-
-};/* class CDSet */
-
-}/* CVC4::context namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__CONTEXT__CDSET_H */
+++ /dev/null
-/********************* */
-/*! \file cdset_forward.h
- ** \verbatim
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief This is a forward declaration header to declare the CDSet<>
- ** template
- **
- ** This is a forward declaration header to declare the CDSet<>
- ** template. It's useful if you want to forward-declare CDSet<>
- ** without including the full cdset.h header, for example, in a
- ** public header context.
- **
- ** For CDSet<> in particular, it's difficult to forward-declare it
- ** yourself, becase it has a default template argument.
- **/
-
-#include "cvc4_public.h"
-
-#ifndef __CVC4__CONTEXT__CDSET_FORWARD_H
-#define __CVC4__CONTEXT__CDSET_FORWARD_H
-
-namespace __gnu_cxx {
- template <class Key> struct hash;
-}/* __gnu_cxx namespace */
-
-namespace CVC4 {
- namespace context {
- template <class V, class HashFcn = __gnu_cxx::hash<V> >
- class CDSet;
- }/* CVC4::context namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__CONTEXT__CDSET_FORWARD_H */
* 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);
#include <ext/hash_map>
-#include "context/cdmap.h"
+#include "context/cdhashmap.h"
namespace CVC4 {
namespace expr {
*/
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) {
}
*/
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,
#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>
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() {
}
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);
}
#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 {
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. */
#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"
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
#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"
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;
#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;
#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"
* 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 {
#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>
//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::CD
HashSet<ArithVar> CDArithVarSet;
class ArithVarCallBack {
public:
#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 {
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);
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;
}
#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"
/**
* 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
#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"
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;
/** 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
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;
#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 {
/** 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;
/**
}
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) {
#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"
}
}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() ){
{
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 */
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;
/** 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;
#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 {
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;
/**
* 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;
/**
#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"
* 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.
/**
* 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).
#include "theory/uf/symmetry_breaker.h"
#include "context/cdo.h"
-#include "context/cdset.h"
+#include "context/cdhashset.h"
namespace CVC4 {
namespace theory {
#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"
// 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
LookupMap d_lookup;
EqMap d_eqMap;
- context::CDSet<TNode, TNodeHashFunction> d_added;
+ context::CDHashSet<TNode, TNodeHashFunction> d_added;
ProofMap d_proof;
ProofLabel d_proofLabel;
* 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 ===
}
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;
#include <map>
#include "context/cdlist.h"
-#include "context/cdmap.h"
+#include "context/cdhashmap.h"
#include "context/cdo.h"
namespace CVC4 {
*/
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:
#include <cxxtest/TestSuite.h>
-#include "context/cdmap.h"
+#include "context/cdhashmap.h"
#include "context/cdlist.h"
using namespace std;
}
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());
// 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);
}
void testObliterate() {
- CDMap<int, int> map(d_context);
+ CDHashMap<int, int> map(d_context);
map.insert(3, 4);
}
void testObliteratePrimordial() {
- CDMap<int, int> map(d_context);
+ CDHashMap<int, int> map(d_context);
map.insert(3, 4);
}
void testObliterateCurrent() {
- CDMap<int, int> map(d_context);
+ CDHashMap<int, int> map(d_context);
map.insert(3, 4);
}
void testInsertAtContextLevelZero() {
- CDMap<int, int> map(d_context);
+ CDHashMap<int, int> map(d_context);
map.insert(3, 4);
}
void testObliterateInsertedAtContextLevelZero() {
- CDMap<int, int> map(d_context);
+ CDHashMap<int, int> map(d_context);
map.insert(3, 4);
//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;
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";
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);
}
#include <cxxtest/TestSuite.h>
-#include "context/cdmap.h"
+#include "context/cdhashmap.h"
#include "util/Assert.h"
using namespace std;
}
void testUnreachableSaveAndRestore() {
- CDMap<int, int> map(d_context);
+ CDHashMap<int, int> map(d_context);
TS_ASSERT_THROWS_NOTHING(map.makeCurrent());
#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"
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) :
}
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 {
projects / cvc5.git / commitdiff