<?fileVersion 4.0.0?>
<cproject storage_type_id="org.eclipse.cdt.core.XmlProjectDescriptionStorage">
-<storageModule moduleId="org.eclipse.cdt.core.settings">
-<cconfiguration id="cdt.managedbuild.toolchain.gnu.base.1461790692">
-<storageModule buildSystemId="org.eclipse.cdt.managedbuilder.core.configurationDataProvider" id="cdt.managedbuild.toolchain.gnu.base.1461790692" moduleId="org.eclipse.cdt.core.settings" name="Default">
-<externalSettings/>
-<extensions>
-<extension id="org.eclipse.cdt.core.ELF" point="org.eclipse.cdt.core.BinaryParser"/>
-<extension id="org.eclipse.cdt.core.MakeErrorParser" point="org.eclipse.cdt.core.ErrorParser"/>
-<extension id="org.eclipse.cdt.core.GCCErrorParser" point="org.eclipse.cdt.core.ErrorParser"/>
-<extension id="org.eclipse.cdt.core.GASErrorParser" point="org.eclipse.cdt.core.ErrorParser"/>
-<extension id="org.eclipse.cdt.core.GLDErrorParser" point="org.eclipse.cdt.core.ErrorParser"/>
-</extensions>
-</storageModule>
-<storageModule moduleId="cdtBuildSystem" version="4.0.0">
-<configuration artifactName="cvc4" buildProperties="" description="" id="cdt.managedbuild.toolchain.gnu.base.1461790692" name="Default" parent="org.eclipse.cdt.build.core.emptycfg">
-<folderInfo id="cdt.managedbuild.toolchain.gnu.base.1461790692.1059214216" name="/" resourcePath="">
-<toolChain id="cdt.managedbuild.toolchain.gnu.base.1311293674" name="cdt.managedbuild.toolchain.gnu.base" superClass="cdt.managedbuild.toolchain.gnu.base">
-<targetPlatform archList="all" binaryParser="org.eclipse.cdt.core.ELF" id="cdt.managedbuild.target.gnu.platform.base.1799734525" name="Debug Platform" osList="linux,hpux,aix,qnx" superClass="cdt.managedbuild.target.gnu.platform.base"/>
-<builder buildPath="${workspace_loc/cvc4/}" id="cdt.managedbuild.target.gnu.builder.base.549477204" incrementalBuildTarget="all" keepEnvironmentInBuildfile="false" managedBuildOn="false" name="Gnu Make Builder" parallelBuildOn="true" parallelizationNumber="2" superClass="cdt.managedbuild.target.gnu.builder.base">
-<outputEntries>
-<entry flags="VALUE_WORKSPACE_PATH|RESOLVED" kind="outputPath" name=""/>
-</outputEntries>
-</builder>
-<tool id="cdt.managedbuild.tool.gnu.archiver.base.888684090" name="GCC Archiver" superClass="cdt.managedbuild.tool.gnu.archiver.base"/>
-<tool id="cdt.managedbuild.tool.gnu.cpp.compiler.base.1803857875" name="GCC C++ Compiler" superClass="cdt.managedbuild.tool.gnu.cpp.compiler.base">
-<inputType id="cdt.managedbuild.tool.gnu.cpp.compiler.input.1333398893" superClass="cdt.managedbuild.tool.gnu.cpp.compiler.input"/>
-</tool>
-<tool id="cdt.managedbuild.tool.gnu.c.compiler.base.1860041504" name="GCC C Compiler" superClass="cdt.managedbuild.tool.gnu.c.compiler.base">
-<inputType id="cdt.managedbuild.tool.gnu.c.compiler.input.814325769" superClass="cdt.managedbuild.tool.gnu.c.compiler.input"/>
-</tool>
-<tool id="cdt.managedbuild.tool.gnu.c.linker.base.1687463194" name="GCC C Linker" superClass="cdt.managedbuild.tool.gnu.c.linker.base"/>
-<tool id="cdt.managedbuild.tool.gnu.cpp.linker.base.709612973" name="GCC C++ Linker" superClass="cdt.managedbuild.tool.gnu.cpp.linker.base">
-<inputType id="cdt.managedbuild.tool.gnu.cpp.linker.input.399338768" superClass="cdt.managedbuild.tool.gnu.cpp.linker.input">
-<additionalInput kind="additionalinputdependency" paths="$(USER_OBJS)"/>
-<additionalInput kind="additionalinput" paths="$(LIBS)"/>
-</inputType>
-</tool>
-<tool id="cdt.managedbuild.tool.gnu.assembler.base.1211277012" name="GCC Assembler" superClass="cdt.managedbuild.tool.gnu.assembler.base">
-<inputType id="cdt.managedbuild.tool.gnu.assembler.input.330956883" superClass="cdt.managedbuild.tool.gnu.assembler.input"/>
-</tool>
-</toolChain>
-</folderInfo>
-<sourceEntries>
-<entry excluding="prop|parser|smt2" flags="VALUE_WORKSPACE_PATH|RESOLVED" kind="sourcePath" name=""/>
-</sourceEntries>
-</configuration>
-</storageModule>
-<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="org.eclipse.cdt.make.core.buildtargets">
-<buildTargets>
-<target name="check" path="" targetID="org.eclipse.cdt.build.MakeTargetBuilder">
-<buildCommand>make</buildCommand>
-<buildArguments/>
-<buildTarget>check</buildTarget>
-<stopOnError>true</stopOnError>
-<useDefaultCommand>true</useDefaultCommand>
-<runAllBuilders>true</runAllBuilders>
-</target>
-</buildTargets>
-</storageModule>
-<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>
-</cconfiguration>
-</storageModule>
-<storageModule moduleId="cdtBuildSystem" version="4.0.0">
-<project id="cvc4.null.1129006228" name="cvc4"/>
-</storageModule>
+ <storageModule moduleId="org.eclipse.cdt.core.settings">
+ <cconfiguration id="cdt.managedbuild.toolchain.gnu.base.1461790692">
+ <storageModule buildSystemId="org.eclipse.cdt.managedbuilder.core.configurationDataProvider" id="cdt.managedbuild.toolchain.gnu.base.1461790692" moduleId="org.eclipse.cdt.core.settings" name="Default">
+ <externalSettings/>
+ <extensions>
+ <extension id="org.eclipse.cdt.core.ELF" point="org.eclipse.cdt.core.BinaryParser"/>
+ <extension id="org.eclipse.cdt.core.GCCErrorParser" point="org.eclipse.cdt.core.ErrorParser"/>
+ <extension id="org.eclipse.cdt.core.GASErrorParser" point="org.eclipse.cdt.core.ErrorParser"/>
+ <extension id="org.eclipse.cdt.core.GLDErrorParser" point="org.eclipse.cdt.core.ErrorParser"/>
+ <extension id="org.eclipse.cdt.core.GmakeErrorParser" point="org.eclipse.cdt.core.ErrorParser"/>
+ <extension id="org.eclipse.cdt.core.CWDLocator" point="org.eclipse.cdt.core.ErrorParser"/>
+ </extensions>
+ </storageModule>
+ <storageModule moduleId="cdtBuildSystem" version="4.0.0">
+ <configuration artifactName="cvc4" buildProperties="" description="" id="cdt.managedbuild.toolchain.gnu.base.1461790692" name="Default" parent="org.eclipse.cdt.build.core.emptycfg">
+ <folderInfo id="cdt.managedbuild.toolchain.gnu.base.1461790692.1059214216" name="/" resourcePath="">
+ <toolChain id="cdt.managedbuild.toolchain.gnu.base.1311293674" name="cdt.managedbuild.toolchain.gnu.base" superClass="cdt.managedbuild.toolchain.gnu.base">
+ <targetPlatform archList="all" binaryParser="org.eclipse.cdt.core.ELF" id="cdt.managedbuild.target.gnu.platform.base.1799734525" name="Debug Platform" osList="linux,hpux,aix,qnx" superClass="cdt.managedbuild.target.gnu.platform.base"/>
+ <builder buildPath="${workspace_loc/cvc4/}" id="cdt.managedbuild.target.gnu.builder.base.549477204" incrementalBuildTarget="all" keepEnvironmentInBuildfile="false" managedBuildOn="false" name="Gnu Make Builder" parallelBuildOn="true" parallelizationNumber="2" superClass="cdt.managedbuild.target.gnu.builder.base">
+ <outputEntries>
+ <entry flags="VALUE_WORKSPACE_PATH|RESOLVED" kind="outputPath" name=""/>
+ </outputEntries>
+ </builder>
+ <tool id="cdt.managedbuild.tool.gnu.archiver.base.888684090" name="GCC Archiver" superClass="cdt.managedbuild.tool.gnu.archiver.base"/>
+ <tool id="cdt.managedbuild.tool.gnu.cpp.compiler.base.1803857875" name="GCC C++ Compiler" superClass="cdt.managedbuild.tool.gnu.cpp.compiler.base">
+ <inputType id="cdt.managedbuild.tool.gnu.cpp.compiler.input.1333398893" superClass="cdt.managedbuild.tool.gnu.cpp.compiler.input"/>
+ </tool>
+ <tool id="cdt.managedbuild.tool.gnu.c.compiler.base.1860041504" name="GCC C Compiler" superClass="cdt.managedbuild.tool.gnu.c.compiler.base">
+ <inputType id="cdt.managedbuild.tool.gnu.c.compiler.input.814325769" superClass="cdt.managedbuild.tool.gnu.c.compiler.input"/>
+ </tool>
+ <tool id="cdt.managedbuild.tool.gnu.c.linker.base.1687463194" name="GCC C Linker" superClass="cdt.managedbuild.tool.gnu.c.linker.base"/>
+ <tool id="cdt.managedbuild.tool.gnu.cpp.linker.base.709612973" name="GCC C++ Linker" superClass="cdt.managedbuild.tool.gnu.cpp.linker.base">
+ <inputType id="cdt.managedbuild.tool.gnu.cpp.linker.input.399338768" superClass="cdt.managedbuild.tool.gnu.cpp.linker.input">
+ <additionalInput kind="additionalinputdependency" paths="$(USER_OBJS)"/>
+ <additionalInput kind="additionalinput" paths="$(LIBS)"/>
+ </inputType>
+ </tool>
+ <tool id="cdt.managedbuild.tool.gnu.assembler.base.1211277012" name="GCC Assembler" superClass="cdt.managedbuild.tool.gnu.assembler.base">
+ <inputType id="cdt.managedbuild.tool.gnu.assembler.input.330956883" superClass="cdt.managedbuild.tool.gnu.assembler.input"/>
+ </tool>
+ </toolChain>
+ </folderInfo>
+ <sourceEntries>
+ <entry excluding="prop|parser|smt2" flags="VALUE_WORKSPACE_PATH|RESOLVED" kind="sourcePath" name=""/>
+ </sourceEntries>
+ </configuration>
+ </storageModule>
+ <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>
</cproject>
type_node.h \
type_node.cpp \
node_builder.h \
- convenience_node_builders.h \
+ convenience_node_builders.h \
type.h \
type.cpp \
node_value.h \
declaration_scope.cpp \
expr_manager_scope.h \
node_self_iterator.h \
- expr_stream.h
+ expr_stream.h \
+ kind_map.h
+
nodist_libexpr_la_SOURCES = \
kind.h \
metakind.h \
--- /dev/null
+/********************* */
+/*! \file kind_map.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 A bitmap of Kinds
+ **
+ ** This is a class representation for a bitmap of Kinds that is
+ ** iterable, manipulable, and packed.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__KIND_MAP_H
+#define __CVC4__KIND_MAP_H
+
+#include <stdint.h>
+#include <iterator>
+
+#include "expr/kind.h"
+
+namespace CVC4 {
+
+/** A bitmap of Kinds. */
+class KindMap {
+ static const size_t SIZE = (kind::LAST_KIND + 63) / 64;
+
+ uint64_t d_bitmap[SIZE];
+
+ /**
+ * Accessor proxy class used so that things like "map[k] = true"
+ * will work as expected (we have to return a proxy from
+ * KindMap::operator[]() in that case, since we can't construct an
+ * address to the individual *bit* in the packed representation).
+ */
+ class Accessor {
+ KindMap& d_map;
+ Kind d_kind;
+
+ Accessor(KindMap& m, Kind k) :
+ d_map(m),
+ d_kind(k) {
+ AssertArgument(k >= Kind(0) && k < kind::LAST_KIND, k, "invalid kind");
+ }
+
+ friend class KindMap;
+
+ public:
+
+ operator bool() const {
+ return d_map.tst(d_kind);
+ }
+
+ Accessor operator=(bool b) const {
+ if(b) {
+ d_map.set(d_kind);
+ } else {
+ d_map.clr(d_kind);
+ }
+ return *this;
+ }
+
+ };/* class KindMap::Accessor */
+
+public:
+
+ /** An iterator over a KindMap. */
+ class iterator {
+ const KindMap* d_map;
+ Kind d_kind;
+
+ public:
+ typedef std::input_iterator_tag iterator_category;
+ typedef Kind value_type;
+
+ iterator() :
+ d_map(NULL),
+ d_kind(Kind(0)) {
+ }
+ iterator(const KindMap& m, Kind k) :
+ d_map(&m),
+ d_kind(k) {
+ AssertArgument(k >= Kind(0) && k <= kind::LAST_KIND, k, "invalid kind");
+ while(d_kind < kind::LAST_KIND &&
+ ! d_map->tst(d_kind)) {
+ d_kind = Kind(uint64_t(d_kind) + 1);
+ }
+ }
+ iterator& operator++() {
+ if(d_kind < kind::LAST_KIND) {
+ d_kind = Kind(uint64_t(d_kind) + 1);
+ while(d_kind < kind::LAST_KIND &&
+ ! d_map->tst(d_kind)) {
+ d_kind = Kind(uint64_t(d_kind) + 1);
+ }
+ }
+ return *this;
+ }
+ iterator operator++(int) const {
+ const_iterator i = *this;
+ ++i;
+ return i;
+ }
+ Kind operator*() const {
+ return d_kind;
+ }
+ bool operator==(iterator i) const {
+ return d_map == i.d_map && d_kind == i.d_kind;
+ }
+ bool operator!=(iterator i) const {
+ return !(*this == i);
+ }
+ };/* class KindMap::iterator */
+ typedef iterator const_iterator;
+
+ KindMap() {
+ clear();
+ }
+ KindMap(const KindMap& m) {
+ for(unsigned i = 0; i < SIZE; ++i) {
+ d_bitmap[i] = m.d_bitmap[i];
+ }
+ }
+ KindMap(Kind k) {
+ clear();
+ set(k);
+ }
+
+ /** Empty the map. */
+ void clear() {
+ for(unsigned i = 0; i < SIZE; ++i) {
+ d_bitmap[i] = uint64_t(0);
+ }
+ }
+ /** Tests whether the map is empty. */
+ bool isEmpty() const {
+ for(unsigned i = 0; i < SIZE; ++i) {
+ if(d_bitmap[i] != uint64_t(0)) {
+ return false;
+ }
+ }
+ return true;
+ }
+ /** Test whether k is in the map. */
+ bool tst(Kind k) const {
+ AssertArgument(k >= Kind(0) && k < kind::LAST_KIND, k, "invalid kind");
+ return (d_bitmap[k / 64] >> (k % 64)) & uint64_t(1);
+ }
+ /** Set k in the map. */
+ void set(Kind k) {
+ AssertArgument(k >= Kind(0) && k < kind::LAST_KIND, k, "invalid kind");
+ d_bitmap[k / 64] |= (uint64_t(1) << (k % 64));
+ }
+ /** Clear k from the map. */
+ void clr(Kind k) {
+ AssertArgument(k >= Kind(0) && k < kind::LAST_KIND, k, "invalid kind");
+ d_bitmap[k / 64] &= ~(uint64_t(1) << (k % 64));
+ }
+
+ /** Iterate over the map. */
+ const_iterator begin() const {
+ return const_iterator(*this, Kind(0));
+ }
+ const_iterator end() const {
+ return const_iterator(*this, kind::LAST_KIND);
+ }
+
+ /** Invert the map. */
+ KindMap operator~() const {
+ KindMap r;
+ for(unsigned i = 0; i < SIZE; ++i) {
+ r.d_bitmap[i] = ~d_bitmap[i];
+ }
+ return r;
+ }
+ /** Bitwise-AND the map (with assignment). */
+ KindMap& operator&=(const KindMap& m) {
+ for(unsigned i = 0; i < SIZE; ++i) {
+ d_bitmap[i] &= m.d_bitmap[i];
+ }
+ return *this;
+ }
+ /** Bitwise-AND the map. */
+ KindMap operator&(const KindMap& m) const {
+ KindMap r(*this);
+ r &= m;
+ return r;
+ }
+ /** Bitwise-OR the map (with assignment). */
+ KindMap& operator|=(const KindMap& m) {
+ for(unsigned i = 0; i < SIZE; ++i) {
+ d_bitmap[i] |= m.d_bitmap[i];
+ }
+ return *this;
+ }
+ /** Bitwise-OR the map. */
+ KindMap operator|(const KindMap& m) const {
+ KindMap r(*this);
+ r |= m;
+ return r;
+ }
+ /** Bitwise-XOR the map (with assignment). */
+ KindMap& operator^=(const KindMap& m) {
+ for(unsigned i = 0; i < SIZE; ++i) {
+ d_bitmap[i] ^= m.d_bitmap[i];
+ }
+ return *this;
+ }
+ /** Bitwise-XOR the map. */
+ KindMap operator^(const KindMap& m) const {
+ KindMap r(*this);
+ r ^= m;
+ return r;
+ }
+
+ /** Test whether k is in the map. */
+ bool operator[](Kind k) const {
+ return tst(k);
+ }
+ /** Test whether k is in the map (allowing assignment). */
+ Accessor operator[](Kind k) {
+ return Accessor(*this, k);
+ }
+
+ /** Test equality between two maps. */
+ bool operator==(KindMap m) {
+ for(unsigned i = 0; i < SIZE; ++i) {
+ if(d_bitmap[i] != m.d_bitmap[i]) {
+ return false;
+ }
+ }
+ return true;
+ }
+ bool operator!=(KindMap m) {
+ return !(*this == m);
+ }
+};/* class KindMap */
+
+inline KindMap operator~(Kind k) {
+ KindMap m(k);
+ return ~m;
+}
+inline KindMap operator&(Kind k1, Kind k2) {
+ KindMap m(k1);
+ return m &= k2;
+}
+inline KindMap operator&(Kind k1, KindMap m2) {
+ return m2 & k1;
+}
+inline KindMap operator|(Kind k1, Kind k2) {
+ KindMap m(k1);
+ return m |= k2;
+}
+inline KindMap operator|(Kind k1, KindMap m2) {
+ return m2 | k1;
+}
+inline KindMap operator^(Kind k1, Kind k2) {
+ KindMap m(k1);
+ return m ^= k2;
+}
+inline KindMap operator^(Kind k1, KindMap m2) {
+ return m2 ^ k1;
+}
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__KIND_MAP_H */
}
}
+bool PropEngine::hasValue(TNode node, bool& value) {
+ Assert(node.getType().isBoolean());
+ SatLiteral lit = d_cnfStream->getLiteral(node);
+
+ SatLiteralValue v = d_satSolver->value(lit);
+ if(v == l_True) {
+ value = true;
+ return true;
+ } else if(v == l_False) {
+ value = false;
+ return true;
+ } else {
+ Assert(v == l_Undef);
+ return false;
+ }
+}
+
+
void PropEngine::push() {
Assert(!d_inCheckSat, "Sat solver in solve()!");
d_satSolver->push();
*/
Node getValue(TNode node);
+ /**
+ * Check if the node has a value and return it if yes.
+ */
+ bool hasValue(TNode node, bool& value);
+
/**
* Push the context level.
*/
#include "theory/booleans/theory_bool.h"
#include "theory/booleans/circuit_propagator.h"
#include "theory/uf/theory_uf.h"
-#include "theory/uf/morgan/theory_uf_morgan.h"
-#include "theory/uf/tim/theory_uf_tim.h"
#include "theory/arith/theory_arith.h"
#include "theory/arrays/theory_arrays.h"
#include "theory/bv/theory_bv.h"
d_theoryEngine->addTheory<theory::arrays::TheoryArrays>();
d_theoryEngine->addTheory<theory::bv::TheoryBV>();
d_theoryEngine->addTheory<theory::datatypes::TheoryDatatypes>();
- switch(Options::current()->uf_implementation) {
- case Options::TIM:
- d_theoryEngine->addTheory<theory::uf::tim::TheoryUFTim>();
- break;
- case Options::MORGAN:
- d_theoryEngine->addTheory<theory::uf::morgan::TheoryUFMorgan>();
- break;
- default:
- Unhandled(Options::current()->uf_implementation);
- }
+ d_theoryEngine->addTheory<theory::uf::TheoryUF>();
d_propEngine = new PropEngine(d_theoryEngine, d_context);
d_theoryEngine->setPropEngine(d_propEngine);
libuf_la_SOURCES = \
theory_uf.h \
+ theory_uf.cpp \
theory_uf_type_rules.h \
theory_uf_rewriter.h
--- /dev/null
+/********************* */
+/*! \file equality_engine.h
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 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 [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_private.h"
+
+#pragma once
+
+#include <queue>
+#include <vector>
+#include <ext/hash_map>
+#include <sstream>
+
+#include "expr/node.h"
+#include "expr/kind_map.h"
+#include "context/cdo.h"
+#include "util/output.h"
+#include "util/stats.h"
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+namespace theory {
+namespace uf {
+
+/** Id of the node */
+typedef size_t EqualityNodeId;
+
+/** Id of the use list */
+typedef size_t UseListNodeId;
+
+/** The trigger ids */
+typedef size_t TriggerId;
+
+/** The equality edge ids */
+typedef size_t EqualityEdgeId;
+
+/** The null node */
+static const EqualityNodeId null_id = (size_t)(-1);
+
+/** The null use list node */
+static const EqualityNodeId null_uselist_id = (size_t)(-1);
+
+/** The null trigger */
+static const TriggerId null_trigger = (size_t)(-1);
+
+/** The null edge id */
+static const EqualityEdgeId null_edge = (size_t)(-1);
+
+/**
+ * A reason for a merge. Either an equality x = y, or a merge of two
+ * function applications f(x1, x2), f(y1, y2)
+ */
+enum MergeReasonType {
+ MERGED_THROUGH_CONGRUENCE,
+ MERGED_THROUGH_EQUALITY
+};
+
+inline std::ostream& operator << (std::ostream& out, MergeReasonType reason) {
+ switch (reason) {
+ case MERGED_THROUGH_CONGRUENCE:
+ out << "c";
+ break;
+ case MERGED_THROUGH_EQUALITY:
+ out << "e";
+ break;
+ default:
+ Unreachable();
+ }
+ return out;
+}
+
+/** A node in the uselist */
+class UseListNode {
+
+private:
+
+ /** The id of the application node where this representative is at */
+ EqualityNodeId d_applicationId;
+
+ /** The next one in the class */
+ UseListNodeId d_nextUseListNodeId;
+
+public:
+
+ /**
+ * Creates a new node, which is in a list of it's own.
+ */
+ UseListNode(EqualityNodeId nodeId, UseListNodeId nextId)
+ : d_applicationId(nodeId), d_nextUseListNodeId(nextId) {}
+
+ /**
+ * Returns the next node in the circular list.
+ */
+ UseListNodeId getNext() const {
+ return d_nextUseListNodeId;
+ }
+
+ /**
+ * Returns the id of the function application.
+ */
+ EqualityNodeId getApplicationId() const {
+ return d_applicationId;
+ }
+};
+
+
+class EqualityNode {
+
+private:
+
+ /** The size of this equivalence class (if it's a representative) */
+ size_t d_size;
+
+ /** The id (in the eq-manager) of the representative equality node */
+ EqualityNodeId d_findId;
+
+ /** The next equality node in this class */
+ EqualityNodeId d_nextId;
+
+ /** The use list of this node */
+ UseListNodeId d_useList;
+
+public:
+
+ /**
+ * Creates a new node, which is in a list of it's own.
+ */
+ EqualityNode(EqualityNodeId nodeId = null_id)
+ : d_size(1), d_findId(nodeId), d_nextId(nodeId), d_useList(null_uselist_id) {}
+
+ /**
+ * Retuerns the uselist.
+ */
+ UseListNodeId getUseList() const {
+ return d_useList;
+ }
+
+ /**
+ * Returns the next node in the class circular list.
+ */
+ EqualityNodeId getNext() const {
+ return d_nextId;
+ }
+
+ /**
+ * Returns the size of this equivalence class (only valid if this is the representative).
+ */
+ size_t getSize() const {
+ return d_size;
+ }
+
+ /**
+ * Merges the two lists. If add size is true the size of this node is increased by the size of
+ * the other node, otherwise the size is decreased by the size of the other node.
+ */
+ template<bool addSize>
+ void merge(EqualityNode& other) {
+ EqualityNodeId tmp = d_nextId; d_nextId = other.d_nextId; other.d_nextId = tmp;
+ if (addSize) {
+ d_size += other.d_size;
+ } else {
+ d_size -= other.d_size;
+ }
+ }
+
+ /**
+ * Returns the class representative.
+ */
+ EqualityNodeId getFind() const { return d_findId; }
+
+ /**
+ * Set the class representative.
+ */
+ void setFind(EqualityNodeId findId) { d_findId = findId; }
+
+ /**
+ * Note that this node is used in a function a application funId.
+ */
+ template<typename memory_class>
+ void usedIn(EqualityNodeId funId, memory_class& memory) {
+ UseListNodeId newUseId = memory.size();
+ memory.push_back(UseListNode(funId, d_useList));
+ d_useList = newUseId;
+ }
+
+};
+
+template <typename NotifyClass>
+class EqualityEngine {
+
+public:
+
+ /** Statistics about the equality engine instance */
+ struct Statistics {
+ /** Total number of merges */
+ IntStat mergesCount;
+ /** Number of terms managed by the system */
+ IntStat termsCount;
+ /** Number of function terms managed by the system */
+ IntStat functionTermsCount;
+ /** Number of times we performed a backtrack */
+ IntStat backtracksCount;
+
+ Statistics(std::string name)
+ : mergesCount(name + "::mergesCount", 0),
+ termsCount(name + "::termsCount", 0),
+ functionTermsCount(name + "::functionTermsCount", 0),
+ backtracksCount(name + "::backtracksCount", 0)
+ {
+ StatisticsRegistry::registerStat(&mergesCount);
+ StatisticsRegistry::registerStat(&termsCount);
+ StatisticsRegistry::registerStat(&functionTermsCount);
+ StatisticsRegistry::registerStat(&backtracksCount);
+ }
+
+ ~Statistics() {
+ StatisticsRegistry::unregisterStat(&mergesCount);
+ StatisticsRegistry::unregisterStat(&termsCount);
+ StatisticsRegistry::unregisterStat(&functionTermsCount);
+ StatisticsRegistry::unregisterStat(&backtracksCount);
+ }
+ };
+
+ /**
+ * f(a,b)
+ */
+ struct FunctionApplication {
+ EqualityNodeId a, b;
+ FunctionApplication(EqualityNodeId a = null_id, EqualityNodeId b = null_id):
+ a(a), b(b) {}
+ bool operator == (const FunctionApplication& other) const {
+ return a == other.a && b == other.b;
+ }
+ bool isApplication() {
+ return a != null_id && b != null_id;
+ }
+ };
+
+ struct FunctionApplicationHashFunction {
+ size_t operator () (const FunctionApplication& app) const {
+ size_t hash = 0;
+ hash = 0x9e3779b9 + app.a;
+ hash ^= 0x9e3779b9 + app.b + (hash << 6) + (hash >> 2);
+ return hash;
+ }
+ };
+
+private:
+
+ /** The class to notify when a representative changes for a term */
+ NotifyClass d_notify;
+
+ /** The map of kinds to be treated as function applications */
+ KindMap d_congruenceKinds;
+
+ /** Map from nodes to their ids */
+ __gnu_cxx::hash_map<TNode, EqualityNodeId, TNodeHashFunction> d_nodeIds;
+
+ /** Map from function applications to their ids */
+ typedef __gnu_cxx::hash_map<FunctionApplication, EqualityNodeId, FunctionApplicationHashFunction> ApplicationIdsMap;
+
+ /**
+ * A map from a pair (a', b') to a function application f(a, b), where a' and b' are the current representatives
+ * of a and b.
+ */
+ ApplicationIdsMap d_applicationLookup;
+
+ /** Map from ids to the nodes */
+ std::vector<TNode> d_nodes;
+
+ /** Map from ids to the nodes */
+ std::vector<FunctionApplication> d_applications;
+
+ /** Map from ids to the equality nodes */
+ std::vector<EqualityNode> d_equalityNodes;
+
+ /** Memory for the use-list nodes */
+ std::vector<UseListNode> d_useListNodes;
+
+ /** Number of asserted equalities we have so far */
+ context::CDO<size_t> d_assertedEqualitiesCount;
+
+ /**
+ * We keep a list of asserted equalities. Not among original terms, but
+ * among the class representatives.
+ */
+ struct Equality {
+ /** Left hand side of the equality */
+ EqualityNodeId lhs;
+ /** Right hand side of the equality */
+ EqualityNodeId rhs;
+ /** Equality constructor */
+ Equality(EqualityNodeId lhs = null_id, EqualityNodeId rhs = null_id)
+ : lhs(lhs), rhs(rhs) {}
+ };
+
+ /** The ids of the classes we have merged */
+ std::vector<Equality> d_assertedEqualities;
+
+ /** The reasons for the equalities */
+
+ /**
+ * An edge in the equality graph. This graph is an undirected graph (both edges added)
+ * containing the actual asserted equalities.
+ */
+ class EqualityEdge {
+
+ // The id of the RHS of this equality
+ EqualityNodeId d_nodeId;
+ // The next edge
+ EqualityEdgeId d_nextId;
+ // Type of reason for this equality
+ MergeReasonType d_mergeType;
+ // Reason of this equality
+ TNode d_reason;
+
+ public:
+
+ EqualityEdge():
+ d_nodeId(null_edge), d_nextId(null_edge), d_mergeType(MERGED_THROUGH_CONGRUENCE) {}
+
+ EqualityEdge(EqualityNodeId nodeId, EqualityNodeId nextId, MergeReasonType type, TNode reason):
+ d_nodeId(nodeId), d_nextId(nextId), d_mergeType(type), d_reason(reason) {}
+
+ /** Returns the id of the next edge */
+ EqualityEdgeId getNext() const { return d_nextId; }
+
+ /** Returns the id of the target edge node */
+ EqualityNodeId getNodeId() const { return d_nodeId; }
+
+ /** The reason of this edge */
+ MergeReasonType getReasonType() const { return d_mergeType; }
+
+ /** The reason of this edge */
+ TNode getReason() const { return d_reason; }
+};
+
+ /**
+ * All the equality edges (twice as many as the number of asserted equalities. If an equality
+ * t1 = t2 is asserted, the edges added are -> t2, -> t1 (in this order). Hance, having the index
+ * of one of the edges you can reconstruct the original equality.
+ */
+ std::vector<EqualityEdge> d_equalityEdges;
+
+ /**
+ * Returns the string representation of the edges.
+ */
+ std::string edgesToString(EqualityEdgeId edgeId) const;
+
+ /**
+ * Map from a node to it's first edge in the equality graph. Edges are added to the front of the
+ * list which makes the insertion/backtracking easy.
+ */
+ std::vector<EqualityEdgeId> d_equalityGraph;
+
+ /** Add an edge to the equality graph */
+ void addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, MergeReasonType type, TNode reason);
+
+ /** Returns the equality node of the given node */
+ EqualityNode& getEqualityNode(TNode node);
+
+ /** Returns the equality node of the given node */
+ EqualityNode& getEqualityNode(EqualityNodeId nodeId);
+
+ /** Returns the id of the node */
+ EqualityNodeId getNodeId(TNode node) const;
+
+ /** Merge the class2 into class1 */
+ void merge(EqualityNode& class1, EqualityNode& class2, std::vector<TriggerId>& triggers);
+
+ /** Undo the mereg of class2 into class1 */
+ void undoMerge(EqualityNode& class1, EqualityNode& class2, EqualityNodeId class2Id);
+
+ /** Backtrack the information if necessary */
+ void backtrack();
+
+ /**
+ * Data used in the BFS search through the equality graph.
+ */
+ struct BfsData {
+ // The current node
+ EqualityNodeId nodeId;
+ // The index of the edge we traversed
+ EqualityEdgeId edgeId;
+ // Index in the queue of the previous node. Shouldn't be too much of them, at most the size
+ // of the biggest equivalence class
+ size_t previousIndex;
+
+ BfsData(EqualityNodeId nodeId = null_id, EqualityEdgeId edgeId = null_edge, size_t prev = 0)
+ : nodeId(nodeId), edgeId(edgeId), previousIndex(prev) {}
+ };
+
+ /**
+ * Trigger that will be updated
+ */
+ struct Trigger {
+ /** The current class id of the LHS of the trigger */
+ EqualityNodeId classId;
+ /** Next trigger for class 1 */
+ TriggerId nextTrigger;
+
+ Trigger(EqualityNodeId classId, TriggerId nextTrigger)
+ : classId(classId), nextTrigger(nextTrigger) {}
+ };
+
+ /**
+ * Vector of triggers (persistent and not-backtrackable). Triggers come in pairs for an
+ * equality trigger (t1, t2): one at position 2k for t1, and one at position 2k + 1 for t2. When
+ * updating triggers we always know where the other one is (^1).
+ */
+ std::vector<Trigger> d_equalityTriggers;
+
+ /**
+ * Vector of original equalities of the triggers.
+ */
+ std::vector<TNode> d_equalityTriggersOriginal;
+
+ /**
+ * Trigger lists per node. The begin id changes as we merge, but the end always points to
+ * the actual end of the triggers for this node.
+ */
+ std::vector<TriggerId> d_nodeTriggers;
+
+ /**
+ * Adds the trigger with triggerId to the beginning of the trigger list of the node with id nodeId.
+ */
+ void addTriggerToList(EqualityNodeId nodeId, TriggerId triggerId);
+
+ /** Statistics */
+ Statistics d_stats;
+
+ /** Add a new function application node to the database, i.e APP t1 t2 */
+ EqualityNodeId newApplicationNode(TNode original, EqualityNodeId t1, EqualityNodeId t2);
+
+ /** Add a new node to the database */
+ EqualityNodeId newNode(TNode t, bool isApplication);
+
+ struct MergeCandidate {
+ EqualityNodeId t1Id, t2Id;
+ MergeReasonType type;
+ TNode reason;
+ MergeCandidate(EqualityNodeId x, EqualityNodeId y, MergeReasonType type, TNode reason):
+ t1Id(x), t2Id(y), type(type), reason(reason) {}
+
+ std::string toString(EqualityEngine& eqEngine) const {
+ std::stringstream ss;
+ ss << eqEngine.d_nodes[t1Id] << " = " << eqEngine.d_nodes[t2Id] << ", " << type;
+ return ss.str();
+ }
+ };
+
+ /** Propagation queue */
+ std::queue<MergeCandidate> d_propagationQueue;
+
+ /** Enqueue to the propagation queue */
+ void enqueue(const MergeCandidate& candidate);
+
+ /** Do the propagation (if check is on, congruences are checked again) */
+ void propagate(bool check);
+
+ /**
+ * Get an explanation of the equality t1 = t2. Returns the asserted equalities that
+ * imply t1 = t2. Returns TNodes as the assertion equalities should be hashed somewhere
+ * else. TODO: mark the phantom equalities (skolems).
+ */
+ void getExplanation(EqualityEdgeId t1Id, EqualityNodeId t2Id, std::vector<TNode>& equalities) const;
+
+ /**
+ * Print the equality graph.
+ */
+ void debugPrintGraph();
+
+public:
+
+ /**
+ * Initialize the equality engine, given the owning class. This will initialize the notifier with
+ * the owner information.
+ */
+ EqualityEngine(NotifyClass& notify, context::Context* context, std::string name)
+ : d_notify(notify), d_assertedEqualitiesCount(context, 0), d_stats(name) {
+ Debug("equality") << "EqualityEdge::EqualityEngine(): id_null = " << +null_id << std::endl;
+ Debug("equality") << "EqualityEdge::EqualityEngine(): edge_null = " << +null_edge << std::endl;
+ Debug("equality") << "EqualityEdge::EqualityEngine(): trigger_null = " << +null_trigger << std::endl;
+ }
+
+ /**
+ * Adds a term to the term database.
+ */
+ void addTerm(TNode t);
+
+ /**
+ * Add a kind to treat as function applications.
+ */
+ void addFunctionKind(Kind fun) {
+ d_congruenceKinds |= fun;
+ }
+
+ /**
+ * Adds a function application term to the database.
+ */
+
+ /**
+ * Check whether the node is already in the database.
+ */
+ bool hasTerm(TNode t) const;
+
+ /**
+ * Adds an equality t1 = t2 to the database.
+ */
+ void addEquality(TNode t1, TNode t2, TNode reason);
+
+ /**
+ * Returns the representative of the term t.
+ */
+ TNode getRepresentative(TNode t) const;
+
+ /**
+ * Returns true if the two nodes are in the same class.
+ */
+ bool areEqual(TNode t1, TNode t2) const;
+
+ /**
+ * Get an explanation of the equality t1 = t2. Returns the asserted equalities that
+ * imply t1 = t2. Returns TNodes as the assertion equalities should be hashed somewhere
+ * else. TODO: mark the phantom equalities (skolems).
+ */
+ void getExplanation(TNode t1, TNode t2, std::vector<TNode>& equalities) const;
+
+ /**
+ * Adds a notify trigger for equality t1 = t2, i.e. when t1 = t2 the notify will be called with
+ * (t1 = t2).
+ */
+ void addTriggerEquality(TNode t1, TNode t2, TNode trigger);
+
+};
+
+} // Namespace uf
+} // Namespace theory
+} // Namespace CVC4
+
--- /dev/null
+/********************* */
+/*! \file equality_engine_impl.h
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 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 [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_private.h"
+
+#pragma once
+
+#include "theory/uf/equality_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace uf {
+
+template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::enqueue(const MergeCandidate& candidate) {
+ Debug("equality") << "EqualityEngine::enqueue(" << candidate.toString(*this) << ")" << std::endl;
+ d_propagationQueue.push(candidate);
+}
+
+template <typename NotifyClass>
+EqualityNodeId EqualityEngine<NotifyClass>::newApplicationNode(TNode original, EqualityNodeId t1, EqualityNodeId t2) {
+ Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << ")" << std::endl;
+
+ ++ d_stats.functionTermsCount;
+
+ // Get another id for this
+ EqualityNodeId funId = newNode(original, true);
+ FunctionApplication fun(t1, t2);
+ d_applications[funId] = fun;
+
+ // The function application we're creating
+ EqualityNodeId t1ClassId = getEqualityNode(t1).getFind();
+ EqualityNodeId t2ClassId = getEqualityNode(t2).getFind();
+ FunctionApplication funNormalized(t1ClassId, t2ClassId);
+
+ // Add the lookup data, if it's not already there
+ typename ApplicationIdsMap::iterator find = d_applicationLookup.find(funNormalized);
+ if (find == d_applicationLookup.end()) {
+ // When we backtrack, if the lookup is not there anymore, we'll add it again
+ Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): no lookup, setting up" << std::endl;
+ d_applicationLookup[funNormalized] = funId;
+ } else {
+ // If it's there, we need to merge these two
+ Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): lookup exists, adding to queue" << std::endl;
+ enqueue(MergeCandidate(funId, find->second, MERGED_THROUGH_CONGRUENCE, TNode::null()));
+ propagate(false);
+ }
+
+ // Add to the use lists
+ d_equalityNodes[t1].usedIn(funId, d_useListNodes);
+ d_equalityNodes[t2].usedIn(funId, d_useListNodes);
+
+ // Return the new id
+ Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << ") => " << funId << std::endl;
+
+ return funId;
+}
+
+template <typename NotifyClass>
+EqualityNodeId EqualityEngine<NotifyClass>::newNode(TNode node, bool isApplication) {
+
+ Debug("equality") << "EqualityEngine::newNode(" << node << ", " << (isApplication ? "function" : "regular") << ")" << std::endl;
+
+ ++ d_stats.termsCount;
+
+ // Register the new id of the term
+ EqualityNodeId newId = d_nodes.size();
+ d_nodeIds[node] = newId;
+ // Add the node to it's position
+ d_nodes.push_back(node);
+ // Note if this is an application or not
+ d_applications.push_back(FunctionApplication());
+ // Add the trigger list for this node
+ d_nodeTriggers.push_back(+null_trigger);
+ // Add it to the equality graph
+ d_equalityGraph.push_back(+null_edge);
+ // Add the equality node to the nodes
+ d_equalityNodes.push_back(EqualityNode(newId));
+
+ Debug("equality") << "EqualityEngine::newNode(" << node << ", " << (isApplication ? "function" : "regular") << ") => " << newId << std::endl;
+
+ return newId;
+}
+
+
+template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::addTerm(TNode t) {
+
+ Debug("equality") << "EqualityEngine::addTerm(" << t << ")" << std::endl;
+
+ // If there already, we're done
+ if (hasTerm(t)) {
+ return;
+ }
+
+ EqualityNodeId result;
+
+ // If a function application we go in
+ if (t.getNumChildren() > 0 && d_congruenceKinds[t.getKind()])
+ {
+ // Add the operator
+ TNode tOp = t.getOperator();
+ addTerm(tOp);
+ // Add all the children and Curryfy
+ result = getNodeId(tOp);
+ for (unsigned i = 0; i < t.getNumChildren(); ++ i) {
+ // Add the child
+ addTerm(t[i]);
+ // Add the application
+ result = newApplicationNode(t, result, getNodeId(t[i]));
+ }
+ } else {
+ // Otherwise we just create the new id
+ result = newNode(t, false);
+ }
+
+ Debug("equality") << "EqualityEngine::addTerm(" << t << ") => " << result << std::endl;
+}
+
+template <typename NotifyClass>
+bool EqualityEngine<NotifyClass>::hasTerm(TNode t) const {
+ return d_nodeIds.find(t) != d_nodeIds.end();
+}
+
+template <typename NotifyClass>
+EqualityNodeId EqualityEngine<NotifyClass>::getNodeId(TNode node) const {
+ Assert(hasTerm(node), node.toString().c_str());
+ return (*d_nodeIds.find(node)).second;
+}
+
+template <typename NotifyClass>
+EqualityNode& EqualityEngine<NotifyClass>::getEqualityNode(TNode t) {
+ return getEqualityNode(getNodeId(t));
+}
+
+template <typename NotifyClass>
+EqualityNode& EqualityEngine<NotifyClass>::getEqualityNode(EqualityNodeId nodeId) {
+ Assert(nodeId < d_equalityNodes.size());
+ return d_equalityNodes[nodeId];
+}
+
+template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::addEquality(TNode t1, TNode t2, TNode reason) {
+
+ Debug("equality") << "EqualityEngine::addEquality(" << t1 << "," << t2 << ")" << std::endl;
+
+ // Backtrack if necessary
+ backtrack();
+
+ // Add the terms if they are not already in the database
+ EqualityNodeId t1Id = getNodeId(t1);
+ EqualityNodeId t2Id = getNodeId(t2);
+
+ // Add to the queue and propagate
+ enqueue(MergeCandidate(t1Id, t2Id, MERGED_THROUGH_EQUALITY, reason));
+ propagate(false);
+}
+
+template <typename NotifyClass>
+TNode EqualityEngine<NotifyClass>::getRepresentative(TNode t) const {
+
+ Debug("equality") << "EqualityEngine::getRepresentative(" << t << ")" << std::endl;
+
+ Assert(hasTerm(t));
+
+ // Both following commands are semantically const
+ const_cast<EqualityEngine*>(this)->backtrack();
+ EqualityNodeId representativeId = const_cast<EqualityEngine*>(this)->getEqualityNode(t).getFind();
+
+ Debug("equality") << "EqualityEngine::getRepresentative(" << t << ") => " << d_nodes[representativeId] << std::endl;
+
+ return d_nodes[representativeId];
+}
+
+template <typename NotifyClass>
+bool EqualityEngine<NotifyClass>::areEqual(TNode t1, TNode t2) const {
+ Debug("equality") << "EqualityEngine::areEqual(" << t1 << "," << t2 << ")" << std::endl;
+
+ Assert(hasTerm(t1));
+ Assert(hasTerm(t2));
+
+ // Both following commands are semantically const
+ const_cast<EqualityEngine*>(this)->backtrack();
+ EqualityNodeId rep1 = const_cast<EqualityEngine*>(this)->getEqualityNode(t1).getFind();
+ EqualityNodeId rep2 = const_cast<EqualityEngine*>(this)->getEqualityNode(t2).getFind();
+
+ Debug("equality") << "EqualityEngine::areEqual(" << t1 << "," << t2 << ") => " << (rep1 == rep2 ? "true" : "false") << std::endl;
+
+ return rep1 == rep2;
+}
+
+template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::merge(EqualityNode& class1, EqualityNode& class2, std::vector<TriggerId>& triggers) {
+
+ Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << ")" << std::endl;
+
+ Assert(triggers.empty());
+
+ ++ d_stats.mergesCount;
+
+ EqualityNodeId class1Id = class1.getFind();
+ EqualityNodeId class2Id = class2.getFind();
+
+ // Update class2 representative information
+ Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): updating class " << class2Id << std::endl;
+ EqualityNodeId currentId = class2Id;
+ do {
+ // Get the current node
+ EqualityNode& currentNode = getEqualityNode(currentId);
+
+ // Update it's find to class1 id
+ Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): " << currentId << "->" << class1Id << std::endl;
+ currentNode.setFind(class1Id);
+
+ // Go through the triggers and inform if necessary
+ TriggerId currentTrigger = d_nodeTriggers[currentId];
+ while (currentTrigger != null_trigger) {
+ Trigger& trigger = d_equalityTriggers[currentTrigger];
+ Trigger& otherTrigger = d_equalityTriggers[currentTrigger ^ 1];
+
+ // If the two are not already in the same class
+ if (otherTrigger.classId != trigger.classId) {
+ trigger.classId = class1Id;
+ // If they became the same, call the trigger
+ if (otherTrigger.classId == class1Id) {
+ // Id of the real trigger is half the internal one
+ triggers.push_back(currentTrigger);
+ }
+ }
+
+ // Go to the next trigger
+ currentTrigger = trigger.nextTrigger;
+ }
+
+ // Move to the next node
+ currentId = currentNode.getNext();
+
+ } while (currentId != class2Id);
+
+
+ // Update class2 table lookup and information
+ Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): updating lookups of " << class2Id << std::endl;
+ do {
+ // Get the current node
+ EqualityNode& currentNode = getEqualityNode(currentId);
+ Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): updating lookups of node " << currentId << std::endl;
+
+ // Go through the uselist and check for congruences
+ UseListNodeId currentUseId = currentNode.getUseList();
+ while (currentUseId != null_uselist_id) {
+ // Get the node of the use list
+ UseListNode& useNode = d_useListNodes[currentUseId];
+ // Get the function application
+ EqualityNodeId funId = useNode.getApplicationId();
+ Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): " << currentId << " in " << d_nodes[funId] << std::endl;
+ const FunctionApplication& fun = d_applications[useNode.getApplicationId()];
+ // Check if there is an application with find arguments
+ EqualityNodeId aNormalized = getEqualityNode(fun.a).getFind();
+ EqualityNodeId bNormalized = getEqualityNode(fun.b).getFind();
+ FunctionApplication funNormalized(aNormalized, bNormalized);
+ typename ApplicationIdsMap::iterator find = d_applicationLookup.find(funNormalized);
+ if (find != d_applicationLookup.end()) {
+ // Applications fun and the funNormalized can be merged due to congruence
+ if (getEqualityNode(funId).getFind() != getEqualityNode(find->second).getFind()) {
+ enqueue(MergeCandidate(funId, find->second, MERGED_THROUGH_CONGRUENCE, TNode::null()));
+ }
+ } else {
+ // There is no representative, so we can add one, we remove this when backtracking
+ d_applicationLookup[funNormalized] = funId;
+ }
+ // Go to the next one in the use list
+ currentUseId = useNode.getNext();
+ }
+
+ // Move to the next node
+ currentId = currentNode.getNext();
+ } while (currentId != class2Id);
+
+ // Now merge the lists
+ class1.merge<true>(class2);
+}
+
+template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::undoMerge(EqualityNode& class1, EqualityNode& class2, EqualityNodeId class2Id) {
+
+ Debug("equality") << "EqualityEngine::undoMerge(" << class1.getFind() << "," << class2Id << ")" << std::endl;
+
+ // Now unmerge the lists (same as merge)
+ class1.merge<false>(class2);
+
+ // First undo the table lookup changes
+ Debug("equality") << "EqualityEngine::undoMerge(" << class1.getFind() << "," << class2Id << "): undoing lookup changes" << std::endl;
+ EqualityNodeId currentId = class2Id;
+ do {
+ // Get the current node
+ EqualityNode& currentNode = getEqualityNode(currentId);
+
+ // Go through the uselist and check for congruences
+ UseListNodeId currentUseId = currentNode.getUseList();
+ while (currentUseId != null_uselist_id) {
+ // Get the node of the use list
+ UseListNode& useNode = d_useListNodes[currentUseId];
+ // Get the function application
+ EqualityNodeId funId = useNode.getApplicationId();
+ const FunctionApplication& fun = d_applications[useNode.getApplicationId()];
+ // Get the application with find arguments
+ EqualityNodeId aNormalized = getEqualityNode(fun.a).getFind();
+ EqualityNodeId bNormalized = getEqualityNode(fun.b).getFind();
+ FunctionApplication funNormalized(aNormalized, bNormalized);
+ typename ApplicationIdsMap::iterator find = d_applicationLookup.find(funNormalized);
+ // If the id is the one we set, then we undo it
+ if (find != d_applicationLookup.end() && find->second == funId) {
+ d_applicationLookup.erase(find);
+ }
+ // Go to the next one in the use list
+ currentUseId = useNode.getNext();
+ }
+
+ // Move to the next node
+ currentId = currentNode.getNext();
+
+ } while (currentId != class2Id);
+
+ // Update class2 representative information
+ Debug("equality") << "EqualityEngine::undoMerge(" << class1.getFind() << "," << class2Id << "): undoing representative info" << std::endl;
+ do {
+ // Get the current node
+ EqualityNode& currentNode = getEqualityNode(currentId);
+
+ // Update it's find to class1 id
+ currentNode.setFind(class2Id);
+
+ // Go through the trigger list (if any) and undo the class
+ TriggerId currentTrigger = d_nodeTriggers[currentId];
+ while (currentTrigger != null_trigger) {
+ Trigger& trigger = d_equalityTriggers[currentTrigger];
+ trigger.classId = class2Id;
+ currentTrigger = trigger.nextTrigger;
+ }
+
+ // Move to the next node
+ currentId = currentNode.getNext();
+
+ } while (currentId != class2Id);
+
+ // Now set any missing lookups and check for any congruences on backtrack
+ std::vector<MergeCandidate> possibleCongruences;
+ Debug("equality") << "EqualityEngine::undoMerge(" << class1.getFind() << "," << class2Id << "): checking for any unset lookups" << std::endl;
+ do {
+ // Get the current node
+ EqualityNode& currentNode = getEqualityNode(currentId);
+
+ // Go through the uselist and check for congruences
+ UseListNodeId currentUseId = currentNode.getUseList();
+ while (currentUseId != null_uselist_id) {
+ // Get the node of the use list
+ UseListNode& useNode = d_useListNodes[currentUseId];
+ // Get the function application
+ EqualityNodeId funId = useNode.getApplicationId();
+ const FunctionApplication& fun = d_applications[useNode.getApplicationId()];
+ // Get the application with find arguments
+ EqualityNodeId aNormalized = getEqualityNode(fun.a).getFind();
+ EqualityNodeId bNormalized = getEqualityNode(fun.b).getFind();
+ FunctionApplication funNormalized(aNormalized, bNormalized);
+ typename ApplicationIdsMap::iterator find = d_applicationLookup.find(funNormalized);
+ Assert(find != d_applicationLookup.end());
+ // If the id doesn't exist, we'll set it
+ if (find == d_applicationLookup.end()) {
+ d_applicationLookup[funNormalized] = funId;
+ } else {
+ // Otherwise, we might be congruent agaain
+ if (getEqualityNode(funId).getFind() != getEqualityNode(find->second).getFind()) {
+ // Damn, we might be merging again, but we'll check this later
+ enqueue(MergeCandidate(funId, find->second, MERGED_THROUGH_CONGRUENCE, TNode::null()));
+ }
+ }
+ // Go to the next one in the use list
+ currentUseId = useNode.getNext();
+ }
+
+ // Move to the next node
+ currentId = currentNode.getNext();
+
+ } while (currentId != class2Id);
+}
+
+template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::backtrack() {
+
+ // If we need to backtrack then do it
+ if (d_assertedEqualitiesCount < d_assertedEqualities.size()) {
+
+ // Clear the propagation queue
+ while (!d_propagationQueue.empty()) {
+ d_propagationQueue.pop();
+ }
+
+ ++ d_stats.backtracksCount;
+
+ Debug("equality") << "EqualityEngine::backtrack(): nodes" << std::endl;
+
+ for (int i = (int)d_assertedEqualities.size() - 1, i_end = (int)d_assertedEqualitiesCount; i >= i_end; --i) {
+ // Get the ids of the merged classes
+ Equality& eq = d_assertedEqualities[i];
+ // Undo the merge
+ undoMerge(d_equalityNodes[eq.lhs], d_equalityNodes[eq.rhs], eq.rhs);
+ }
+
+ d_assertedEqualities.resize(d_assertedEqualitiesCount);
+
+ Debug("equality") << "EqualityEngine::backtrack(): edges" << std::endl;
+
+ for (int i = (int)d_equalityEdges.size() - 2, i_end = (int)(2*d_assertedEqualitiesCount); i >= i_end; i -= 2) {
+ EqualityEdge& edge1 = d_equalityEdges[i];
+ EqualityEdge& edge2 = d_equalityEdges[i | 1];
+ d_equalityGraph[edge2.getNodeId()] = edge1.getNext();
+ d_equalityGraph[edge1.getNodeId()] = edge2.getNext();
+ }
+
+ d_equalityEdges.resize(2 * d_assertedEqualitiesCount);
+
+ // Now repropagate if something got reenqueued
+ propagate(true);
+ }
+}
+
+template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, MergeReasonType type, TNode reason) {
+ Debug("equality") << "EqualityEngine::addGraphEdge(" << d_nodes[t1] << "," << d_nodes[t2] << "," << reason << ")" << std::endl;
+ EqualityEdgeId edge = d_equalityEdges.size();
+ d_equalityEdges.push_back(EqualityEdge(t2, d_equalityGraph[t1], type, reason));
+ d_equalityEdges.push_back(EqualityEdge(t1, d_equalityGraph[t2], type, reason));
+ d_equalityGraph[t1] = edge;
+ d_equalityGraph[t2] = edge | 1;
+
+ if (Debug.isOn("equality::internal")) {
+ const_cast<EqualityEngine*>(this)->debugPrintGraph();
+ }
+}
+
+template <typename NotifyClass>
+std::string EqualityEngine<NotifyClass>::edgesToString(EqualityEdgeId edgeId) const {
+ std::stringstream out;
+ bool first = true;
+ if (edgeId == null_edge) {
+ out << "null";
+ } else {
+ while (edgeId != null_edge) {
+ const EqualityEdge& edge = d_equalityEdges[edgeId];
+ if (!first) out << ",";
+ out << d_nodes[edge.getNodeId()];
+ edgeId = edge.getNext();
+ first = false;
+ }
+ }
+ return out.str();
+}
+
+template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::getExplanation(TNode t1, TNode t2, std::vector<TNode>& equalities) const {
+ Assert(getRepresentative(t1) == getRepresentative(t2));
+
+ Debug("equality") << "EqualityEngine::getExplanation(" << t1 << "," << t2 << ")" << std::endl;
+
+ // Backtrack if necessary
+ const_cast<EqualityEngine*>(this)->backtrack();
+
+ // Get the explanation
+ EqualityNodeId t1Id = getNodeId(t1);
+ EqualityNodeId t2Id = getNodeId(t2);
+ getExplanation(t1Id, t2Id, equalities);
+}
+
+template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, std::vector<TNode>& equalities) const {
+
+ Debug("equality") << "EqualityEngine::getExplanation(" << d_nodes[t1Id] << "," << d_nodes[t2Id] << ")" << std::endl;
+
+ // If the nodes are the same, we're done
+ if (t1Id == t2Id) return;
+
+ if (Debug.isOn("equality::internal")) {
+ const_cast<EqualityEngine*>(this)->debugPrintGraph();
+ }
+
+ // Queue for the BFS containing nodes
+ std::vector<BfsData> bfsQueue;
+
+ // Find a path from t1 to t2 in the graph (BFS)
+ bfsQueue.push_back(BfsData(t1Id, null_id, 0));
+ size_t currentIndex = 0;
+ while (true) {
+ // There should always be a path, and every node can be visited only once (tree)
+ Assert(currentIndex < bfsQueue.size());
+
+ // The next node to visit
+ BfsData current = bfsQueue[currentIndex];
+ EqualityNodeId currentNode = current.nodeId;
+
+ Debug("equality") << "EqualityEngine::getExplanation(): currentNode = " << d_nodes[currentNode] << std::endl;
+
+ // Go through the equality edges of this node
+ EqualityEdgeId currentEdge = d_equalityGraph[currentNode];
+ Debug("equality") << "EqualityEngine::getExplanation(): edgesId = " << currentEdge << std::endl;
+ Debug("equality") << "EqualityEngine::getExplanation(): edges = " << edgesToString(currentEdge) << std::endl;
+
+ while (currentEdge != null_edge) {
+ // Get the edge
+ const EqualityEdge& edge = d_equalityEdges[currentEdge];
+
+ // If not just the backwards edge
+ if ((currentEdge | 1u) != (current.edgeId | 1u)) {
+
+ Debug("equality") << "EqualityEngine::getExplanation(): currentEdge = (" << d_nodes[currentNode] << "," << d_nodes[edge.getNodeId()] << ")" << std::endl;
+
+ // Did we find the path
+ if (edge.getNodeId() == t2Id) {
+
+ Debug("equality") << "EqualityEngine::getExplanation(): path found: " << std::endl;
+
+ // Reconstruct the path
+ do {
+ // The current node
+ currentNode = bfsQueue[currentIndex].nodeId;
+ EqualityNodeId edgeNode = d_equalityEdges[currentEdge].getNodeId();
+ MergeReasonType reasonType = d_equalityEdges[currentEdge].getReasonType();
+
+ Debug("equality") << "EqualityEngine::getExplanation(): currentEdge = " << currentEdge << ", currentNode = " << currentNode << std::endl;
+
+ // Add the actual equality to the vector
+ if (reasonType == MERGED_THROUGH_CONGRUENCE) {
+ // f(x1, x2) == f(y1, y2) because x1 = y1 and x2 = y2
+ Debug("equality") << "EqualityEngine::getExplanation(): due to congruence, going deeper" << std::endl;
+ const FunctionApplication& f1 = d_applications[currentNode];
+ const FunctionApplication& f2 = d_applications[edgeNode];
+ Debug("equality") << push;
+ getExplanation(f1.a, f2.a, equalities);
+ getExplanation(f1.b, f2.b, equalities);
+ Debug("equality") << pop;
+ } else {
+ // Construct the equality
+ Debug("equality") << "EqualityEngine::getExplanation(): adding: " << d_equalityEdges[currentEdge].getReason() << std::endl;
+ equalities.push_back(d_equalityEdges[currentEdge].getReason());
+ }
+
+ // Go to the previous
+ currentEdge = bfsQueue[currentIndex].edgeId;
+ currentIndex = bfsQueue[currentIndex].previousIndex;
+ } while (currentEdge != null_id);
+
+ // Done
+ return;
+ }
+
+ // Push to the visitation queue if it's not the backward edge
+ bfsQueue.push_back(BfsData(edge.getNodeId(), currentEdge, currentIndex));
+ }
+
+ // Go to the next edge
+ currentEdge = edge.getNext();
+ }
+
+ // Go to the next node to visit
+ ++ currentIndex;
+ }
+}
+
+template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::addTriggerEquality(TNode t1, TNode t2, TNode trigger) {
+
+ Debug("equality") << "EqualityEngine::addTrigger(" << t1 << ", " << t2 << ", " << trigger << ")" << std::endl;
+
+ Assert(hasTerm(t1));
+ Assert(hasTerm(t2));
+
+ // Get the information about t1
+ EqualityNodeId t1Id = getNodeId(t1);
+ EqualityNodeId t1classId = getEqualityNode(t1Id).getFind();
+ TriggerId t1TriggerId = d_nodeTriggers[t1Id];
+
+ // Get the information about t2
+ EqualityNodeId t2Id = getNodeId(t2);
+ EqualityNodeId t2classId = getEqualityNode(t2Id).getFind();
+ TriggerId t2TriggerId = d_nodeTriggers[t2Id];
+
+ Debug("equality") << "EqualityEngine::addTrigger(" << trigger << "): " << t1Id << " (" << t1classId << ") = " << t2Id << " (" << t2classId << ")" << std::endl;
+
+ // Create the triggers
+ TriggerId t1NewTriggerId = d_equalityTriggers.size();
+ TriggerId t2NewTriggerId = t1NewTriggerId | 1;
+ d_equalityTriggers.push_back(Trigger(t1classId, t1TriggerId));
+ d_equalityTriggersOriginal.push_back(trigger);
+ d_equalityTriggers.push_back(Trigger(t2classId, t2TriggerId));
+ d_equalityTriggersOriginal.push_back(trigger);
+
+ // Add the trigger to the trigger graph
+ d_nodeTriggers[t1Id] = t1NewTriggerId;
+ d_nodeTriggers[t2Id] = t2NewTriggerId;
+
+ // If the trigger is already on, we propagate
+ if (t1classId == t2classId) {
+ Debug("equality") << "EqualityEngine::addTrigger(" << t1 << "," << t2 << "): triggered at setup time" << std::endl;
+ d_notify.notifyEquality(trigger); // Don't care about the return value
+ }
+
+ Debug("equality") << "EqualityEngine::addTrigger(" << t1 << "," << t2 << ") => (" << t1NewTriggerId << ", " << t2NewTriggerId << ")" << std::endl;
+}
+
+template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::propagate(bool check) {
+
+ Debug("equality") << "EqualityEngine::propagate()" << std::endl;
+
+ bool done = false;
+ while (!d_propagationQueue.empty()) {
+
+ // The current merge candidate
+ const MergeCandidate current = d_propagationQueue.front();
+ d_propagationQueue.pop();
+
+ if (done) {
+ // If we're done, just empty the queue
+ continue;
+ }
+
+ // Get the representatives
+ EqualityNodeId t1classId = getEqualityNode(current.t1Id).getFind();
+ EqualityNodeId t2classId = getEqualityNode(current.t2Id).getFind();
+
+ // If already the same, we're done
+ if (t1classId == t2classId) {
+ continue;
+ }
+
+ // If check is on, and a congruence, check the arguments (it might be from a backtrack)
+ if (check && current.type == MERGED_THROUGH_CONGRUENCE) {
+ const FunctionApplication& f1 = d_applications[current.t1Id];
+ const FunctionApplication& f2 = d_applications[current.t2Id];
+ if (getEqualityNode(f1.a).getFind() != getEqualityNode(f2.a).getFind()) continue;
+ if (getEqualityNode(f1.b).getFind() != getEqualityNode(f2.b).getFind()) continue;
+ }
+
+ // Get the nodes of the representatives
+ EqualityNode& node1 = getEqualityNode(t1classId);
+ EqualityNode& node2 = getEqualityNode(t2classId);
+
+ Assert(node1.getFind() == t1classId);
+ Assert(node2.getFind() == t2classId);
+
+ // Depending on the merge preference (such as size), merge them
+ std::vector<TriggerId> triggers;
+ if (node2.getSize() > node1.getSize()) {
+ Debug("equality") << "EqualityEngine::propagate(): merging " << d_nodes[current.t1Id]<< " into " << d_nodes[current.t2Id] << std::endl;
+ merge(node2, node1, triggers);
+ d_assertedEqualities.push_back(Equality(t2classId, t1classId));
+ } else {
+ Debug("equality") << "EqualityEngine::propagate(): merging " << d_nodes[current.t2Id] << " into " << d_nodes[current.t1Id] << std::endl;
+ merge(node1, node2, triggers);
+ d_assertedEqualities.push_back(Equality(t1classId, t2classId));
+ }
+
+ // Add the actuall equality to the equality graph
+ addGraphEdge(current.t1Id, current.t2Id, current.type, current.reason);
+
+ // One more equality added
+ d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1;
+
+ Assert(2*d_assertedEqualities.size() == d_equalityEdges.size());
+ Assert(d_assertedEqualities.size() == d_assertedEqualitiesCount);
+
+ // Notify the triggers
+ for (size_t trigger = 0, trigger_end = triggers.size(); trigger < trigger_end && !done; ++ trigger) {
+ // Notify the trigger and exit if it fails
+ done = !d_notify.notifyEquality(d_equalityTriggersOriginal[triggers[trigger]]);
+ }
+ }
+}
+
+template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::debugPrintGraph() {
+ for (EqualityNodeId nodeId = 0; nodeId < d_nodes.size(); ++ nodeId) {
+
+ Debug("equality::internal") << d_nodes[nodeId] << " " << nodeId << "(" << getEqualityNode(nodeId).getFind() << "):";
+
+ EqualityEdgeId edgeId = d_equalityGraph[nodeId];
+ while (edgeId != null_edge) {
+ const EqualityEdge& edge = d_equalityEdges[edgeId];
+ Debug("equality::internal") << " " << d_nodes[edge.getNodeId()] << ":" << edge.getReason();
+ edgeId = edge.getNext();
+ }
+
+ Debug("equality::internal") << std::endl;
+ }
+}
+
+} // Namespace uf
+} // Namespace theory
+} // Namespace CVC4
+
--- /dev/null
+/********************* */
+/*! \file theory_uf.cpp
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 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 the interface to TheoryUF implementations
+ **
+ ** This is the interface to TheoryUF implementations. All
+ ** implementations of TheoryUF should inherit from this class.
+ **/
+
+#include "theory/uf/theory_uf.h"
+#include "theory/uf/equality_engine_impl.h"
+
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::theory::uf;
+
+using namespace std;
+
+Node mkAnd(const std::vector<TNode>& conjunctions) {
+ Assert(conjunctions.size() > 0);
+
+ std::set<TNode> all;
+ all.insert(conjunctions.begin(), conjunctions.end());
+
+ if (all.size() == 1) {
+ // All the same, or just one
+ return conjunctions[0];
+ }
+
+ NodeBuilder<> conjunction(kind::AND);
+ std::set<TNode>::const_iterator it = all.begin();
+ std::set<TNode>::const_iterator it_end = all.end();
+ while (it != it_end) {
+ conjunction << *it;
+ ++ it;
+ }
+
+ return conjunction;
+}
+
+void TheoryUF::check(Effort level) {
+
+ while (!done() && !d_conflict) {
+ // Get all the assertions
+ TNode assertion = get();
+ Debug("uf") << "TheoryUF::check(): processing " << assertion << std::endl;
+
+ // Fo the work
+ switch (assertion.getKind()) {
+ case kind::EQUAL:
+ d_equalityEngine.addEquality(assertion[0], assertion[1], assertion);
+ break;
+ case kind::APPLY_UF:
+ d_equalityEngine.addEquality(assertion, d_true, assertion);
+ case kind::NOT:
+ if (assertion[0].getKind() == kind::APPLY_UF) {
+ d_equalityEngine.addEquality(assertion[0], d_false, assertion);
+ }
+ break;
+ default:
+ Unreachable();
+ }
+ }
+
+ // If in conflict, output the conflict
+ if (d_conflict) {
+ Debug("uf") << "TheoryUF::check(): conflict " << d_conflictNode << std::endl;
+ d_out->conflict(d_conflictNode);
+ d_literalsToPropagate.clear();
+ }
+
+ // Otherwise we propagate in order to detect a weird conflict like
+ // p, x = y
+ // p -> f(x) != f(y) -- f(x) = f(y) gets added to the propagation list at preregistration time
+ // but when f(x) != f(y) is deduced by the sat solver, so it's asserted, and we don't detect the conflict
+ // until we go through the propagation list
+ propagate(level);
+}
+
+void TheoryUF::propagate(Effort level) {
+ Debug("uf") << "TheoryUF::propagate()" << std::endl;
+ if (!d_conflict) {
+ for (unsigned i = 0; i < d_literalsToPropagate.size(); ++ i) {
+ TNode literal = d_literalsToPropagate[i];
+ Debug("uf") << "TheoryUF::propagate(): propagating " << literal << std::endl;
+ bool satValue;
+ if (!d_valuation.hasSatValue(literal, satValue)) {
+ d_out->propagate(literal);
+ } else {
+ std::vector<TNode> assumptions;
+ if (literal != d_false) {
+ TNode negatedLiteral = literal.getKind() == kind::NOT ? literal[0] : (TNode) literal.notNode();
+ assumptions.push_back(negatedLiteral);
+ }
+ explain(literal, assumptions);
+ d_conflictNode = mkAnd(assumptions);
+ d_conflict = true;
+ break;
+ }
+ }
+ }
+ d_literalsToPropagate.clear();
+}
+
+void TheoryUF::preRegisterTerm(TNode node) {
+ Debug("uf") << "TheoryUF::preRegisterTerm(" << node << ")" << std::endl;
+
+ switch (node.getKind()) {
+ case kind::EQUAL:
+ // Add the terms
+ d_equalityEngine.addTerm(node[0]);
+ d_equalityEngine.addTerm(node[1]);
+ // Add the trigger
+ d_equalityEngine.addTriggerEquality(node[0], node[1], node);
+ break;
+ case kind::APPLY_UF:
+ // Function applications/predicates
+ d_equalityEngine.addTerm(node);
+ // Maybe it's a predicate
+ if (node.getType().isBoolean()) {
+ // Get triggered for both equal and dis-equal
+ d_equalityEngine.addTriggerEquality(node, d_true, node);
+ d_equalityEngine.addTriggerEquality(node, d_false, node.notNode());
+ }
+ default:
+ // Variables etc
+ d_equalityEngine.addTerm(node);
+ break;
+ }
+}
+
+bool TheoryUF::propagate(TNode atom, bool isTrue) {
+ Debug("uf") << "TheoryUF::propagate(" << atom << ", " << (isTrue ? "true" : "false" ) << ")" << std::endl;
+
+ // If already in conflict, no more propagation
+ if (d_conflict) {
+ Debug("uf") << "TheoryUF::propagate(" << atom << ", " << (isTrue ? "true" : "false" ) << "): already in conflict" << std::endl;
+ return false;
+ }
+
+ // The literal
+ TNode literal = isTrue ? (Node) atom : atom.notNode();
+
+ // See if the literal has been asserted already
+ bool satValue = false;
+ bool isAsserted = literal == d_false || d_valuation.hasSatValue(literal, satValue);
+
+ // If asserted, we're done or in conflict
+ if (isAsserted) {
+ if (satValue) {
+ Debug("uf") << "TheoryUF::propagate(" << atom << ", " << (isTrue ? "true" : "false" ) << ") => already known" << std::endl;
+ return true;
+ } else {
+ Debug("uf") << "TheoryUF::propagate(" << atom << ", " << (isTrue ? "true" : "false" ) << ") => conflict" << std::endl;
+ std::vector<TNode> assumptions;
+ if (literal != d_false) {
+ TNode negatedLiteral = isTrue ? atom.notNode() : (Node) atom;
+ assumptions.push_back(negatedLiteral);
+ }
+ explain(literal, assumptions);
+ d_conflictNode = mkAnd(assumptions);
+ d_conflict = true;
+ return false;
+ }
+ }
+
+ // Nothing, just enqueue it for propagation and mark it as asserted already
+ Debug("uf") << "TheoryUF::propagate(" << atom << ", " << (isTrue ? "true" : "false" ) << ") => enqueuing for propagation" << std::endl;
+ d_literalsToPropagate.push_back(literal);
+
+ return true;
+}
+
+void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions) {
+ TNode lhs, rhs;
+ switch (literal.getKind()) {
+ case kind::EQUAL:
+ lhs = literal[0];
+ rhs = literal[1];
+ break;
+ case kind::APPLY_UF:
+ lhs = literal;
+ rhs = d_true;
+ break;
+ case kind::NOT:
+ lhs = literal[0];
+ rhs = d_false;
+ case kind::CONST_BOOLEAN:
+ // we get to explain true = false, since we set false to be the trigger of this
+ lhs = d_true;
+ rhs = d_false;
+ break;
+ default:
+ Unreachable();
+ }
+ d_equalityEngine.getExplanation(lhs, rhs, assumptions);
+}
+
+void TheoryUF::explain(TNode literal) {
+ Debug("uf") << "TheoryUF::explain(" << literal << ")" << std::endl;
+ std::vector<TNode> assumptions;
+ explain(literal, assumptions);
+ d_out->explanation(mkAnd(assumptions));
+}
/********************* */
/*! \file theory_uf.h
** \verbatim
- ** Original author: mdeters
+ ** Original author: dejan
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
#include "expr/attribute.h"
#include "theory/theory.h"
+#include "theory/uf/equality_engine.h"
-#include "context/context.h"
+#include "context/cdo.h"
+#include "context/cdset.h"
namespace CVC4 {
namespace theory {
namespace uf {
class TheoryUF : public Theory {
+
+public:
+
+ class NotifyClass {
+ TheoryUF& d_uf;
+ public:
+ NotifyClass(TheoryUF& uf): d_uf(uf) {}
+
+ bool notifyEquality(TNode eq) {
+ Debug("uf") << "NotifyClass::notifyEquality(" << eq << ")" << std::endl;
+ // Just forward to uf
+ return d_uf.propagate(eq, true);
+ }
+ };
+
+private:
+
+ /** The notify class */
+ NotifyClass d_notify;
+
+ /** Equaltity engine */
+ EqualityEngine<NotifyClass> d_equalityEngine;
+
+ /** All the literals known to be true */
+ context::CDSet<TNode, TNodeHashFunction> d_knownFacts;
+
+ /** Are we in conflict */
+ context::CDO<bool> d_conflict;
+
+ /** The conflict node */
+ Node d_conflictNode;
+
+ /**
+ * Should be called to propagate the atom. If isTrue is true, the atom should be propagated,
+ * otherwise the negated atom should be propagated.
+ */
+ bool propagate(TNode atom, bool isTrue);
+
+ /**
+ * Explain why this literal is true by adding assumptions
+ */
+ void explain(TNode literal, std::vector<TNode>& assumptions);
+
+ /** Literals to propagate */
+ std::vector<TNode> d_literalsToPropagate;
+
+ /** True node for predicates = true */
+ Node d_true;
+
+ /** True node for predicates = false */
+ Node d_false;
+
public:
/** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
- TheoryUF(context::Context* ctxt, OutputChannel& out, Valuation valuation)
- : Theory(THEORY_UF, ctxt, out, valuation) { }
-
- // We declare these here (even though it's not terribly useful) for
- // documentation reasons, and to keep mktheorytraits from issuing a
- // spurious warning.
- virtual void check(Effort) = 0;
- virtual void propagate(Effort) {}
- virtual void staticLearning(TNode in, NodeBuilder<>& learned) {}
- virtual void notifyRestart() {}
- virtual void presolve() {}
+ TheoryUF(context::Context* ctxt, OutputChannel& out, Valuation valuation):
+ Theory(THEORY_UF, ctxt, out, valuation),
+ d_notify(*this),
+ d_equalityEngine(d_notify, ctxt, "theory::uf::TheoryUF"),
+ d_knownFacts(ctxt),
+ d_conflict(ctxt, false)
+ {
+ // The kinds we are treating as function application in congruence
+ d_equalityEngine.addFunctionKind(kind::APPLY_UF);
+
+ // The boolean constants
+ d_true = NodeManager::currentNM()->mkConst<bool>(true);
+ d_false = NodeManager::currentNM()->mkConst<bool>(false);
+ d_equalityEngine.addTerm(d_true);
+ d_equalityEngine.addTerm(d_false);
+ d_equalityEngine.addTriggerEquality(d_true, d_false, d_false);
+ }
+
+ void check(Effort);
+ void propagate(Effort);
+ void preRegisterTerm(TNode term);
+ void explain(TNode n);
+
+ std::string identify() const {
+ return "THEORY_UF";
+ }
};/* class TheoryUF */
return d_engine->getValue(n);
}
+bool Valuation::hasSatValue(TNode n, bool& value) const {
+ return d_engine->getPropEngine()->hasValue(n, value);
+}
+
Node Valuation::getSatValue(TNode n) const{
if(n.getKind() == kind::NOT) {
Node atomRes = d_engine->getPropEngine()->getValue(n[0]);
*/
Node getSatValue(TNode n) const;
+ /**
+ * Returns true if the node has a sat value. If yes value is set to it's value.
+ */
+ bool hasSatValue(TNode n, bool& value) const;
+
};/* class Valuation */
}/* CVC4::theory namespace */
eq_diamond1.smt \
eq_diamond14.reduced.smt \
eq_diamond14.reduced2.smt \
- eq_diamond23.smt \
NEQ016_size5_reduced2a.smt \
NEQ016_size5_reduced2b.smt \
dead_dnd002.smt \
projects / cvc5.git / commitdiff