专利快速检索-快速检索全球专利，免费商用专利数据库-IPRDB

1. 发明申请

US20090192767A1 MODEL-BASED THEORY COMBINATION 失效
标题翻译：基于模型的理论组合
公开(公告)号：US20090192767A1
公开(公告)日：2009-07-30
申请号：US12019500
申请日：2008-01-24
申请人： Leonardo M. de Moura , Nikolaj S. Bjorner
发明人： Leonardo M. de Moura , Nikolaj S. Bjorner
IPC分类号： G06F17/10
CPC分类号： G06F17/10
摘要： A method is described for combining models of a plurality of theory solvers in order to produce a model which may be satisfiable by each of the plurality of theory solvers. A model is accessed for a first theory solver which is satisfiable in the first theory solver. It is determined that one or more equalities are implied by the model and it is determined if the equalities are compatible with a second solver. The model is updated in accordance any equalities determined not to be compatible with the second solver. A method is also described for mutation of models using freedom intervals. A freedom interval is determined for a variable within a model and the model is updates by choosing a value for the variable which lies within the freedom interval.
摘要翻译：描述了用于组合多个理论解算器的模型的方法，以便产生可由多个理论解算器中的每一个满足的模型。第一个理论解算器访问一个模型，在第一个理论解算器中可以满足。确定模型隐含一个或多个等式，并且确定该等式是否与第二求解器兼容。该模型根据确定不与第二个求解器兼容的任何均等进行更新。还描述了使用自由间隔的模型突变的方法。为模型中的变量确定自由间隔，并且通过选择位于自由间隔内的变量的值来更新模型。

2. 发明申请

US20090164501A1 E-MATCHING FOR SMT SOLVERS 有权
标题翻译： SMT解决方案的电子匹配
公开(公告)号：US20090164501A1
公开(公告)日：2009-06-25
申请号：US11962847
申请日：2007-12-21
申请人： Leonardo M. de Moura , Nikolaj S. Bjorner
发明人： Leonardo M. de Moura , Nikolaj S. Bjorner
IPC分类号： G06F17/30
CPC分类号： G06F8/443
摘要： Embodiments are introduced which provide for creation of an E-matching code tree index which works on E-graphs to make E-matching more efficient. Use of the E-matching code tree allows performing matching of several patterns simultaneously. Embodiments are also described which provide for the generation of inverted path indexes. An inverted path index may be used to filter an E-graph to determine terms which may potentially match patterns when an E-graph is updated.
摘要翻译：实施例提供了用于创建E匹配代码树索引，其在E图上工作以使E匹配更有效。使用电子匹配代码树可以同时执行几种模式的匹配。还描述了提供反向路径索引的生成的实施例。可以使用反向路径索引来过滤E图以确定当E图更新时可能潜在匹配模式的术语。

3. 发明授权

US08103674B2 E-matching for SMT solvers 有权
标题翻译： SMT求解器的电子匹配
公开(公告)号：US08103674B2
公开(公告)日：2012-01-24
申请号：US11962847
申请日：2007-12-21
申请人： Leonardo M. de Moura , Nikolaj S. Bjorner
发明人： Leonardo M. de Moura , Nikolaj S. Bjorner
IPC分类号： G06F17/30
CPC分类号： G06F8/443
摘要： Embodiments are introduced which provide for creation of an E-matching code tree index which works on E-graphs to make E-matching more efficient. Use of the E-matching code tree allows performing matching of several patterns simultaneously. Embodiments are also described which provide for the generation of inverted path indexes. An inverted path index may be used to filter an E-graph to determine terms which may potentially match patterns when an E-graph is updated.
摘要翻译：实施例提供了用于创建E匹配代码树索引，其在E图上工作以使E匹配更有效。使用电子匹配代码树可以同时执行几种模式的匹配。还描述了提供反向路径索引的生成的实施例。可以使用反向路径索引来过滤E图以确定当E图更新时可能潜在匹配模式的术语。

4. 发明授权

US07925476B2 Model-based theory combination 失效
标题翻译：基于模型的理论组合
公开(公告)号：US07925476B2
公开(公告)日：2011-04-12
申请号：US12019500
申请日：2008-01-24
申请人： Leonardo M. de Moura , Nikolaj S. Bjorner
发明人： Leonardo M. de Moura , Nikolaj S. Bjorner
IPC分类号： G06F7/60 , G06F17/10
CPC分类号： G06F17/10
摘要： A method is described for combining models of a plurality of theory solvers in order to produce a model which may be satisfiable by each of the plurality of theory solvers. A model is accessed for a first theory solver which is satisfiable in the first theory solver. It is determined that one or more equalities are implied by the model and it is determined if the equalities are compatible with a second solver. The model is updated in accordance any equalities determined not to be compatible with the second solver. A method is also described for mutation of models using freedom intervals. A freedom interval is determined for a variable within a model and the model is updates by choosing a value for the variable which lies within the freedom interval.
摘要翻译：描述了用于组合多个理论解算器的模型的方法，以便产生可由多个理论解算器中的每一个满足的模型。第一个理论解算器访问一个模型，在第一个理论解算器中可以满足。确定模型隐含一个或多个等式，并且确定该等式是否与第二求解器兼容。该模型根据确定不与第二个求解器兼容的任何均等进行更新。还描述了使用自由间隔的模型突变的方法。为模型中的变量确定自由间隔，并且通过选择位于自由间隔内的变量的值来更新模型。

5. 发明申请

US20110161937A1 PROCESSING PREDICATES INCLUDING POINTER INFORMATION 有权
标题翻译：处理预测包括指针信息
公开(公告)号：US20110161937A1
公开(公告)日：2011-06-30
申请号：US12649335
申请日：2009-12-30
申请人： Eleonora O. Bounimova , Vladimir A. Levin , Leonardo M. de Moura , Thomas J. Ball
发明人： Eleonora O. Bounimova , Vladimir A. Levin , Leonardo M. de Moura , Thomas J. Ball
IPC分类号： G06F9/44
CPC分类号： G06F8/313 , G06F8/434 , G06F11/3608
摘要： A system is described for processing predicates in the course of analyzing a program, based on a general-purpose theory of pointers. The system converts location expressions in the predicates into logical formulae that are interpretable by a theorem prover module, producing converted predicates. This conversion associates the location expressions with location objects. More specifically, the conversion represents variables as explicitly-specified location objects, and location terms (such as a field-type access terms and dereference-type terms) as constructor-specified location objects. The theory of pointers is also expressed by a set of axioms which constrain the operation of the theorem prover module.
摘要翻译：描述了一种基于指针的通用理论在分析程序过程中处理谓词的系统。系统将谓词中的位置表达式转换为可由定理证明器模块解释的逻辑公式，从而产生转换的谓词。此转换将位置表达式与位置对象相关联。更具体地说，转换表示作为显式指定的位置对象的变量，以及作为构造器指定的位置对象的位置术语（诸如字段类型访问术语和解引用类型术语）。指针理论也由限定定理证明器模块操作的一组公理表示。

6. 发明授权

US08595707B2 Processing predicates including pointer information 有权
标题翻译：处理谓词包括指针信息
公开(公告)号：US08595707B2
公开(公告)日：2013-11-26
申请号：US12649335
申请日：2009-12-30
申请人： Eleonora O. Bounimova , Vladimir A. Levin , Leonardo M. de Moura , Thomas J. Ball
发明人： Eleonora O. Bounimova , Vladimir A. Levin , Leonardo M. de Moura , Thomas J. Ball
IPC分类号： G06F17/24
CPC分类号： G06F8/313 , G06F8/434 , G06F11/3608
摘要： A system is described for processing predicates in the course of analyzing a program, based on a general-purpose theory of pointers. The system converts location expressions in the predicates into logical formulae that are interpretable by a theorem prover module, producing converted predicates. This conversion associates the location expressions with location objects. More specifically, the conversion represents variables as explicitly-specified location objects, and location terms (such as a field-type access terms and dereference-type terms) as constructor-specified location objects. The theory of pointers is also expressed by a set of axioms which constrain the operation of the theorem prover module.
摘要翻译：描述了一种基于指针的通用理论在分析程序过程中处理谓词的系统。系统将谓词中的位置表达式转换为可由定理证明器模块解释的逻辑公式，从而产生转换的谓词。此转换将位置表达式与位置对象相关联。更具体地说，转换表示作为显式指定的位置对象的变量，以及作为构造器指定的位置对象的位置术语（诸如字段类型访问术语和解引用类型术语）。指针理论也由限定定理证明器模块操作的一组公理表示。

你已经成功收藏专利！

检索式保存成功!

IPRDB

热门服务

关于我们

友情链接

联系方式