专利快速检索-快速检索全球专利，免费商用专利数据库-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. 发明授权

US08473895B2 Providing diverse solutions using design space exploration 有权
标题翻译：使用设计空间探索提供多种解决方案
公开(公告)号：US08473895B2
公开(公告)日：2013-06-25
申请号：US12795669
申请日：2010-06-08
申请人： Ethan K. Jackson , Wolfram Schulte , Nikolaj S. Bjorner , Eunsuk Kang
发明人： Ethan K. Jackson , Wolfram Schulte , Nikolaj S. Bjorner , Eunsuk Kang
IPC分类号： G06F9/44
CPC分类号： G06F17/5045 , G06F2217/08
摘要： A design space exploration (DSE) system automatically discovers viable solutions within a design space. The DSE system operates by creating or receiving a design specification that is described using a design language. The design specification contains a collection of constraints that an acceptable architecture is expected to satisfy. The DSE system then symbolically executes the design specification to provide a logical formula. The DSE system then interacts with a theorem prover module to identify one or more solutions to the formula. Finally, the DSE system converts the solutions into a user-interpretable form (e.g., expressed in the format of the modeling language) for viewing by a user. Each solution pertains to an architecture that satisfies the collection of constraints. The DSE system ensures that the solutions are diverse by disfavoring any solution that is deemed similar to any solution that has been previously encountered.
摘要翻译：设计空间探索（DSE）系统在设计空间内自动发现可行的解决方案。 DSE系统通过创建或接收使用设计语言描述的设计规范进行操作。设计规范包含可接受架构预期满足的约束集合。 DSE系统然后象征性地执行设计规范以提供逻辑公式。然后，DSE系统与定理证明器模块进行交互，以识别公式的一个或多个解决方案。最后，DSE系统将解决方案转换成用户可解释的形式（例如，以建模语言的格式表示），以供用户观看。每个解决方案都涉及满足约束集合的体系结构。 DSE系统确保解决方案是多样的，因为不满意任何与以前遇到过的解决方案相似的解决方案。

6. 发明申请

US20110302550A1 Providing Diverse Solutions Using Design Space Exploration 有权
标题翻译：使用设计空间探索提供不同的解决方案
公开(公告)号：US20110302550A1
公开(公告)日：2011-12-08
申请号：US12795669
申请日：2010-06-08
申请人： Ethan K. Jackson , Wolfram Schulte , Nikolaj S. Bjorner , Eunsuk Kang
发明人： Ethan K. Jackson , Wolfram Schulte , Nikolaj S. Bjorner , Eunsuk Kang
IPC分类号： G06F9/44
CPC分类号： G06F17/5045 , G06F2217/08
摘要： A design space exploration (DSE) system automatically discovers viable solutions within a design space. The DSE system operates by creating or receiving a design specification that is described using a design language. The design specification contains a collection of constraints that an acceptable architecture is expected to satisfy. The DSE system then symbolically executes the design specification to provide a logical formula. The DSE system then interacts with a theorem prover module to identify one or more solutions to the formula. Finally, the DSE system converts the solutions into a user-interpretable form (e.g., expressed in the format of the modeling language) for viewing by a user. Each solution pertains to an architecture that satisfies the collection of constraints. The DSE system ensures that the solutions are diverse by disfavoring any solution that is deemed similar to any solution that has been previously encountered.
摘要翻译：设计空间探索（DSE）系统在设计空间内自动发现可行的解决方案。 DSE系统通过创建或接收使用设计语言描述的设计规范进行操作。设计规范包含可接受架构预期满足的约束集合。 DSE系统然后象征性地执行设计规范以提供逻辑公式。然后，DSE系统与定理证明器模块进行交互，以识别公式的一个或多个解决方案。最后，DSE系统将解决方案转换成用户可解释的形式（例如，以建模语言的格式表示），以供用户观看。每个解决方案都涉及满足约束集合的体系结构。 DSE系统确保解决方案是多样的，因为不满意任何与以前遇到过的解决方案相似的解决方案。

7. 发明授权

US07660833B2 Granular control over the authority of replicated information via fencing and unfencing 有权
标题翻译：通过围栏和不合格对复制信息的权威进行细致的控制
公开(公告)号：US07660833B2
公开(公告)日：2010-02-09
申请号：US10733459
申请日：2003-12-10
申请人： Dan Teodosiu , Nikolaj S. Bjorner
发明人： Dan Teodosiu , Nikolaj S. Bjorner
IPC分类号： G06F12/00
CPC分类号： G06F17/30215 , Y10S707/99954
摘要： A method and system for controlling which content gets precedence and is replicated. A replica set is comprised of a set of resources. Each resource is associated with resource data and resource meta-data. For files-based systems, resource data includes file contents and attributes, while resource meta-data includes additional attributes that are relevant for negotiating synchronization during replication. An extra field called a “fence value” is added to the meta-data associated with each resource. During synchronization, first fence values are compared. The resource with the highest fence value includes the content that is controlling and replicated. If fence values are equal (and greater than a particular value), the controlling resource is determined based on other meta-data.
摘要翻译：用于控制哪些内容优先并被复制的方法和系统。副本集由一组资源组成。每个资源与资源数据和资源元数据相关联。对于基于文件的系统，资源数据包括文件内容和属性，而资源元数据包括与复制期间协商同步相关的附加属性。称为“栅栏值”的额外字段被添加到与每个资源相关联的元数据。在同步期间，比较第一个围栏值。栅栏值最高的资源包括正在控制和复制的内容。如果围栏值相等（并且大于特定值），则基于其他元数据确定控制资源。

8. 发明申请

US20090328015A1 Matching Based Pattern Inference for SMT Solvers 有权
标题翻译： SMT求解器匹配模式推理
公开(公告)号：US20090328015A1
公开(公告)日：2009-12-31
申请号：US12146373
申请日：2008-06-25
申请人： Nikolaj S. Bjorner , Leonardo Mendonca de Moura
发明人： Nikolaj S. Bjorner , Leonardo Mendonca de Moura
IPC分类号： G06F9/45
CPC分类号： G06F9/44589
摘要： A method for automatically analyzing formulas and adding pattern annotations to quantifiers based on a database of common pattern idioms. The method involves matching base pattern inference for Satisfiability Modulo Theories (SMT) solvers. The method uses a database for fault detection in externally supplied pattern annotated formulas. The method also uses matching code trees to mixed second-order pattern matching.
摘要翻译：一种基于公共模式习语的数据库自动分析公式并向量词添加模式注释的方法。该方法涉及匹配基本模式推理的可满足性模理论（SMT）求解器。该方法使用外部提供的模式注释公式中的故障检测数据库。该方法还使用匹配代码树来混合二阶模式匹配。

9. 发明授权

US07072982B2 Universal naming scheme for peer to peer resources 失效
公开(公告)号：US07072982B2
公开(公告)日：2006-07-04
申请号：US09952808
申请日：2001-09-13
申请人： Dan Teodosiu , Nikolaj S. Bjorner , Markus M. Breunig
发明人： Dan Teodosiu , Nikolaj S. Bjorner , Markus M. Breunig
IPC分类号： G05F15/16
CPC分类号： H04L61/1552 , H04L29/12066 , H04L29/12132 , H04L61/1511 , H04L67/104 , H04L67/1046 , H04L67/1063
摘要： Peer devices register with a resource locator service so that the peer devices can be uniquely identified in a networking environment. An addressing scheme addresses a peer resource in the networking environment based on the unique identifier of a peer device that is a master publisher of the resource. Based on the addressing scheme, the resource locator service can track the location of the master publisher of the resource as well as additional locations of peer devices that have cached the resource and made it available. In various embodiments, the resource locator service can service requests for peer resources by providing a list of locations where the resource is expected to be available or, in the case of non-compatible requester, provide access to the resource itself.

10. 发明授权

US09489221B2 Matching based pattern inference for SMT solvers 有权
标题翻译：针对SMT求解器的匹配模式推理
公开(公告)号：US09489221B2
公开(公告)日：2016-11-08
申请号：US12146373
申请日：2008-06-25
申请人： Nikolaj S. Bjorner , Leonardo Mendonca de Moura
发明人： Nikolaj S. Bjorner , Leonardo Mendonca de Moura
IPC分类号： G06F9/44 , G06F9/445
CPC分类号： G06F9/44589
摘要： A method for automatically analyzing formulas and adding pattern annotations to quantifiers based on a database of common pattern idioms. The method involves matching base pattern inference for Satisfiability Modulo Theories (SMT) solvers. The method uses a database for fault detection in externally supplied pattern annotated formulas. The method also uses matching code trees to mixed second-order pattern matching.
摘要翻译：一种基于公共模式习语的数据库自动分析公式并向量词添加模式注释的方法。该方法涉及匹配基本模式推理的可满足性模理论（SMT）求解器。该方法使用外部提供的模式注释公式中的故障检测数据库。该方法还使用匹配代码树来混合二阶模式匹配。

你已经成功收藏专利！

检索式保存成功!

IPRDB

热门服务

关于我们

友情链接

联系方式