小编Jon*_*gan的帖子

这是我的Makefile的简化版本:

.PHONY: all 

all: src/server.coffee
  mkdir -p bin
  ./node_modules/.bin/coffee -c -o bin src/server.coffee

我想运行make,只有在src/server.coffee更改后才重新编译.但是,每次运行时它都会重新编译make:

$ make
mkdir -p bin
./node_modules/.bin/coffee -c -o bin src/server.coffee
$ make
mkdir -p bin
./node_modules/.bin/coffee -c -o bin src/server.coffee

如果我将Makefile更改为不使用虚假目标,它将按预期工作.新的Makefile:

bin/server.js: src/server.coffee
  mkdir -p bin
  ./node_modules/.bin/coffee -c -o bin src/server.coffee

结果:

$ make
mkdir -p bin
./node_modules/.bin/coffee -c -o bin src/server.coffee
$ make
make: `bin/server.js' is up to date.

为什么它不尊重我对虚假目标的依赖？我问的原因是因为实际上,我不会将单个文件编译成单个其他文件,因此我不想跟踪所有输出文件的名称以用作目标.

我有一些简单的约束,涉及生成的z3中的实数乘法unknown.问题似乎是它们被包装在数据类型中,因为展开的版本会产生sat.

这是一个简化的案例:

(declare-datatypes () ((T (NUM (n Real)))))

(declare-const a T)
(declare-const b T)
(declare-const c T)

(assert (is-NUM a))
(assert (is-NUM b))
(assert (is-NUM c))

(assert (= c (NUM (* (n a) (n b)))))

(check-sat)
;unknown

没有数据类型:

(declare-const a Real)
(declare-const b Real)
(declare-const c Real)

(assert (= c (* a b)))

(check-sat)
;sat

我正在使用z3 3.2,但这也可以在网络界面中重现.